0 JBC
↳1 JBC2FIG (⇒)
↳2 JBCTerminationGraph
↳3 FIGtoITRSProof (⇒)
↳4 AND
↳5 IDP
↳6 IDPtoQDPProof (⇒)
↳7 QDP
↳8 QDPSizeChangeProof (⇔)
↳9 YES
↳10 IDP
↳11 IDPtoQDPProof (⇒)
↳12 QDP
↳13 UsableRulesProof (⇔)
↳14 QDP
↳15 QReductionProof (⇔)
↳16 QDP
↳17 QDPSizeChangeProof (⇔)
↳18 YES
↳19 IDP
↳20 IDPNonInfProof (⇒)
↳21 AND
↳22 IDP
↳23 IDependencyGraphProof (⇔)
↳24 TRUE
↳25 IDP
↳26 IDependencyGraphProof (⇔)
↳27 TRUE
↳28 IDP
↳29 IDPNonInfProof (⇒)
↳30 AND
↳31 IDP
↳32 IDependencyGraphProof (⇔)
↳33 TRUE
↳34 IDP
↳35 IDependencyGraphProof (⇔)
↳36 TRUE
public class Test5 {
public static void main(String[] args) {
List l1 = List.mk(args.length);
List l2 = List.mk(args.length + 3);
List l3 = List.mk(args.length + 5);
List temp;
while (length(l1) > 0) {
temp = l1;
l1 = l2;
l2 = l3;
l3 = temp;
if (length(l2) % 3 == 0)
temp = temp.getTail();
if (length(l3) % 5 == 0)
l3 = l3.getTail();
if (length(l1) > length(l2))
l1 = l1.getTail();
else if (length(l1) == length(l2))
l2 = l2.getTail();
else
l3 = l3.getTail();
test(l1, l2, l3);
}
}
private static int length(List list) {
int len = 0;
while (list != null) {
list = list.getTail();
len++;
}
return len;
}
private static void test(List l1, List l2, List l3) {
while (l1 != null) {
l2 = new List(l1, l2);
l3 = new List(l2, l3);
l1 = l1.getTail();
}
}
}
public class List {
public Object head;
private List tail;
public List(Object head, List tail) {
this.head = head;
this.tail = tail;
}
public List getTail() {
return tail;
}
public static List mk(int len) {
List result = null;
while (len-- > 0)
result = new List(new Object(), result);
return result;
}
}
Generated 51 rules for P and 2 rules for R.
Combined rules. Obtained 3 rules for P and 0 rules for R.
Filtered ground terms:
3187_0_test_NULL(x1, x2, x3, x4, x5) → 3187_0_test_NULL(x2, x3, x4, x5)
List(x1, x2) → List(x2)
2415_0_test_NULL(x1, x2, x3, x4, x5) → 2415_0_test_NULL(x2, x3, x4, x5)
Filtered duplicate args:
3187_0_test_NULL(x1, x2, x3, x4) → 3187_0_test_NULL(x2, x3, x4)
2415_0_test_NULL(x1, x2, x3, x4) → 2415_0_test_NULL(x2, x3, x4)
Finished conversion. Obtained 3 rules for P and 0 rules for R. System has no predefined symbols.
Generated 19 rules for P and 3 rules for R.
Combined rules. Obtained 3 rules for P and 1 rules for R.
Filtered ground terms:
707_0_length_Store(x1, x2) → 707_0_length_Store(x2)
627_0_length_NULL(x1, x2, x3) → 627_0_length_NULL(x2, x3)
List(x1, x2) → List(x2)
656_0_length_Return(x1) → 656_0_length_Return
Filtered duplicate args:
627_0_length_NULL(x1, x2) → 627_0_length_NULL(x2)
Finished conversion. Obtained 3 rules for P and 1 rules for R. System has no predefined symbols.
Generated 23 rules for P and 3 rules for R.
Combined rules. Obtained 1 rules for P and 0 rules for R.
Filtered ground terms:
422_0_mk_Inc(x1, x2, x3) → 422_0_mk_Inc(x2, x3)
Cond_422_0_mk_Inc(x1, x2, x3, x4) → Cond_422_0_mk_Inc(x1, x3, x4)
Filtered duplicate args:
422_0_mk_Inc(x1, x2) → 422_0_mk_Inc(x2)
Cond_422_0_mk_Inc(x1, x2, x3) → Cond_422_0_mk_Inc(x1, x3)
Combined rules. Obtained 1 rules for P and 0 rules for R.
Finished conversion. Obtained 1 rules for P and 0 rules for R. System has predefined symbols.
Generated 114 rules for P and 206 rules for R.
Combined rules. Obtained 12 rules for P and 16 rules for R.
Filtered ground terms:
List(x1, x2) → List(x2)
718_0_length_ConstantStackPush(x1, x2) → 718_0_length_ConstantStackPush(x2)
656_0_length_Return(x1, x2) → 656_0_length_Return(x2)
775_0_length_ConstantStackPush(x1, x2) → 775_0_length_ConstantStackPush(x2)
1100_0_test_Load(x1, x2, x3, x4) → 1100_0_test_Load(x2, x3, x4)
233_0_length_ConstantStackPush(x1, x2) → 233_0_length_ConstantStackPush(x2)
2429_0_test_Return(x1) → 2429_0_test_Return
908_0_length_ConstantStackPush(x1, x2) → 908_0_length_ConstantStackPush(x2)
867_0_length_ConstantStackPush(x1, x2) → 867_0_length_ConstantStackPush(x2)
807_0_length_ConstantStackPush(x1, x2) → 807_0_length_ConstantStackPush(x2)
668_0_length_ConstantStackPush(x1, x2) → 668_0_length_ConstantStackPush(x2)
2390_0_test_NULL(x1, x2, x3, x4, x5) → 2390_0_test_NULL(x2, x3, x4, x5)
3158_0_test_NULL(x1, x2, x3, x4, x5) → 3158_0_test_NULL(x2, x3, x4, x5)
627_0_length_NULL(x1, x2, x3, x4) → 627_0_length_NULL(x2, x3, x4)
Cond_627_0_length_NULL(x1, x2, x3, x4, x5) → Cond_627_0_length_NULL(x1, x3, x4, x5)
697_0_getTail_Return(x1, x2) → 697_0_getTail_Return(x2)
Filtered duplicate args:
718_1_main_InvokeMethod(x1, x2, x3, x4, x5) → 718_1_main_InvokeMethod(x1, x2, x3, x5)
Cond_668_1_main_InvokeMethod1(x1, x2, x3, x4, x5, x6, x7) → Cond_668_1_main_InvokeMethod1(x1, x2, x3, x6, x7)
668_1_main_InvokeMethod(x1, x2, x3, x4, x5, x6) → 668_1_main_InvokeMethod(x1, x2, x5, x6)
775_1_main_InvokeMethod(x1, x2, x3, x4, x5) → 775_1_main_InvokeMethod(x1, x3, x4, x5)
Cond_718_1_main_InvokeMethod1(x1, x2, x3, x4, x5, x6) → Cond_718_1_main_InvokeMethod1(x1, x2, x3, x4, x6)
1100_1_main_InvokeMethod(x1, x2, x3, x4, x5, x6, x7) → 1100_1_main_InvokeMethod(x1, x5, x6, x7)
Cond_807_1_main_InvokeMethod1(x1, x2, x3, x4, x5, x6, x7) → Cond_807_1_main_InvokeMethod1(x1, x2, x3, x5, x6, x7)
807_1_main_InvokeMethod(x1, x2, x3, x4, x5, x6) → 807_1_main_InvokeMethod(x1, x2, x4, x5, x6)
908_1_main_InvokeMethod(x1, x2, x3, x4, x5, x6) → 908_1_main_InvokeMethod(x1, x2, x4, x5, x6)
233_1_main_InvokeMethod(x1, x2, x3, x4, x5) → 233_1_main_InvokeMethod(x1, x3, x4, x5)
Cond_908_1_main_InvokeMethod(x1, x2, x3, x4, x5, x6, x7) → Cond_908_1_main_InvokeMethod(x1, x2, x3, x5, x6, x7)
867_1_main_InvokeMethod(x1, x2, x3, x4, x5) → 867_1_main_InvokeMethod(x1, x3, x4, x5)
Cond_807_1_main_InvokeMethod(x1, x2, x3, x4, x5, x6, x7) → Cond_807_1_main_InvokeMethod(x1, x2, x3, x5, x6, x7)
Cond_718_1_main_InvokeMethod(x1, x2, x3, x4, x5, x6) → Cond_718_1_main_InvokeMethod(x1, x2, x3, x4, x6)
Cond_668_1_main_InvokeMethod(x1, x2, x3, x4, x5, x6, x7) → Cond_668_1_main_InvokeMethod(x1, x2, x3, x6, x7)
Cond_233_1_main_InvokeMethod(x1, x2, x3, x4, x5, x6) → Cond_233_1_main_InvokeMethod(x1, x2, x4, x5, x6)
2390_0_test_NULL(x1, x2, x3, x4) → 2390_0_test_NULL(x2, x3, x4)
3158_0_test_NULL(x1, x2, x3, x4) → 3158_0_test_NULL(x2, x3, x4)
627_0_length_NULL(x1, x2, x3) → 627_0_length_NULL(x2, x3)
Cond_627_0_length_NULL(x1, x2, x3, x4) → Cond_627_0_length_NULL(x1, x3, x4)
Filtered unneeded arguments:
Cond_807_1_main_InvokeMethod(x1, x2, x3, x4, x5, x6) → Cond_807_1_main_InvokeMethod(x1, x2, x3, x4, x6)
Cond_908_1_main_InvokeMethod(x1, x2, x3, x4, x5, x6) → Cond_908_1_main_InvokeMethod(x1, x2, x3, x4, x6)
Cond_807_1_main_InvokeMethod1(x1, x2, x3, x4, x5, x6) → Cond_807_1_main_InvokeMethod1(x1, x2, x3, x4, x6)
Combined rules. Obtained 12 rules for P and 15 rules for R.
Finished conversion. Obtained 12 rules for P and 15 rules for R. System has predefined symbols.
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
(0) -> (1), if ((java.lang.Object(List(x1[0])) →* x1[1])∧(java.lang.Object(List(x2[0])) →* x2[1])∧(java.lang.Object(x0[0]) →* java.lang.Object(List(java.lang.Object(x0[1])))))
(0) -> (2), if ((java.lang.Object(List(x1[0])) →* x1[2])∧(java.lang.Object(List(x2[0])) →* x2[2])∧(java.lang.Object(x0[0]) →* java.lang.Object(List(x0[2]))))
(1) -> (1), if ((java.lang.Object(List(x1[1])) →* x1[1]')∧(java.lang.Object(List(x2[1])) →* x2[1]')∧(java.lang.Object(x0[1]) →* java.lang.Object(List(java.lang.Object(x0[1]')))))
(1) -> (2), if ((java.lang.Object(List(x1[1])) →* x1[2])∧(java.lang.Object(List(x2[1])) →* x2[2])∧(java.lang.Object(x0[1]) →* java.lang.Object(List(x0[2]))))
(2) -> (0), if ((java.lang.Object(List(x1[2])) →* java.lang.Object(List(x1[0])))∧(java.lang.Object(List(x2[2])) →* java.lang.Object(List(x2[0])))∧(x0[2] →* java.lang.Object(x0[0])))
3187_0_TEST_NULL(java.lang.Object(List(x1[0])), java.lang.Object(List(x2[0])), java.lang.Object(x0[0])) → 2415_0_TEST_NULL(java.lang.Object(List(x1[0])), java.lang.Object(List(x2[0])), java.lang.Object(x0[0]))
2415_0_TEST_NULL(x1[1], x2[1], java.lang.Object(List(java.lang.Object(x0[1])))) → 2415_0_TEST_NULL(java.lang.Object(List(x1[1])), java.lang.Object(List(x2[1])), java.lang.Object(x0[1]))
2415_0_TEST_NULL(x1[2], x2[2], java.lang.Object(List(x0[2]))) → 3187_0_TEST_NULL(java.lang.Object(List(x1[2])), java.lang.Object(List(x2[2])), x0[2])
From the DPs we obtained the following set of size-change graphs:
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
(0) -> (1), if ((x0[0] →* java.lang.Object(List(x0[1]))))
(0) -> (2), if ((x0[0] →* java.lang.Object(List(x0[2]))))
(1) -> (1), if ((x0[1] →* java.lang.Object(List(x0[1]'))))
(1) -> (2), if ((x0[1] →* java.lang.Object(List(x0[2]))))
(2) -> (0), if ((x0[2] →* x0[0]))
707_0_LENGTH_STORE(x0[0]) → 627_0_LENGTH_NULL(x0[0])
627_0_LENGTH_NULL(java.lang.Object(List(x0[1]))) → 627_0_LENGTH_NULL(x0[1])
627_0_LENGTH_NULL(java.lang.Object(List(x0[2]))) → 707_0_LENGTH_STORE(x0[2])
627_0_length_NULL(NULL) → 656_0_length_Return
627_0_length_NULL(NULL)
707_0_LENGTH_STORE(x0[0]) → 627_0_LENGTH_NULL(x0[0])
627_0_LENGTH_NULL(java.lang.Object(List(x0[1]))) → 627_0_LENGTH_NULL(x0[1])
627_0_LENGTH_NULL(java.lang.Object(List(x0[2]))) → 707_0_LENGTH_STORE(x0[2])
627_0_length_NULL(NULL)
627_0_length_NULL(NULL)
707_0_LENGTH_STORE(x0[0]) → 627_0_LENGTH_NULL(x0[0])
627_0_LENGTH_NULL(java.lang.Object(List(x0[1]))) → 627_0_LENGTH_NULL(x0[1])
627_0_LENGTH_NULL(java.lang.Object(List(x0[2]))) → 707_0_LENGTH_STORE(x0[2])
From the DPs we obtained the following set of size-change graphs:
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
(0) -> (1), if ((x0[0] > 0 →* TRUE)∧(x0[0] →* x0[1]))
(1) -> (0), if ((x0[1] + -1 →* x0[0]))
(1) (>(x0[0], 0)=TRUE∧x0[0]=x0[1] ⇒ 422_0_MK_INC(x0[0])≥NonInfC∧422_0_MK_INC(x0[0])≥COND_422_0_MK_INC(>(x0[0], 0), x0[0])∧(UIncreasing(COND_422_0_MK_INC(>(x0[0], 0), x0[0])), ≥))
(2) (>(x0[0], 0)=TRUE ⇒ 422_0_MK_INC(x0[0])≥NonInfC∧422_0_MK_INC(x0[0])≥COND_422_0_MK_INC(>(x0[0], 0), x0[0])∧(UIncreasing(COND_422_0_MK_INC(>(x0[0], 0), x0[0])), ≥))
(3) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_422_0_MK_INC(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(4) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_422_0_MK_INC(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(5) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_422_0_MK_INC(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(6) (x0[0] ≥ 0 ⇒ (UIncreasing(COND_422_0_MK_INC(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8 + (2)bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(7) (COND_422_0_MK_INC(TRUE, x0[1])≥NonInfC∧COND_422_0_MK_INC(TRUE, x0[1])≥422_0_MK_INC(+(x0[1], -1))∧(UIncreasing(422_0_MK_INC(+(x0[1], -1))), ≥))
(8) ((UIncreasing(422_0_MK_INC(+(x0[1], -1))), ≥)∧[2 + (-1)bso_11] ≥ 0)
(9) ((UIncreasing(422_0_MK_INC(+(x0[1], -1))), ≥)∧[2 + (-1)bso_11] ≥ 0)
(10) ((UIncreasing(422_0_MK_INC(+(x0[1], -1))), ≥)∧[2 + (-1)bso_11] ≥ 0)
(11) ((UIncreasing(422_0_MK_INC(+(x0[1], -1))), ≥)∧0 = 0∧[2 + (-1)bso_11] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = 0
POL(422_0_MK_INC(x1)) = [2]x1
POL(COND_422_0_MK_INC(x1, x2)) = [2]x2
POL(>(x1, x2)) = [-1]
POL(0) = 0
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]
COND_422_0_MK_INC(TRUE, x0[1]) → 422_0_MK_INC(+(x0[1], -1))
422_0_MK_INC(x0[0]) → COND_422_0_MK_INC(>(x0[0], 0), x0[0])
422_0_MK_INC(x0[0]) → COND_422_0_MK_INC(>(x0[0], 0), x0[0])
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer, Boolean
(0) -> (1), if ((x0[0] > 0 →* TRUE)∧(656_0_length_Return(x0[0]) →* 656_0_length_Return(x0[1]))∧(x2[0] →* x2[1])∧(x3[0] →* x3[1])∧(x1[0] →* x1[1]))
(1) -> (2), if ((233_0_length_ConstantStackPush(x3[1]) →* 656_0_length_Return(x0[2]))∧(x2[1] →* x1[2])∧(x1[1] →* x3[2])∧(x3[1] →* x2[2]))
(1) -> (18), if ((233_0_length_ConstantStackPush(x3[1]) →* 656_0_length_Return(x0[18]))∧(x2[1] →* x1[18])∧(x1[1] →* java.lang.Object(List(x3[18])))∧(x3[1] →* x2[18]))
(2) -> (3), if ((!(x0[2] % 3 = 0) →* TRUE)∧(656_0_length_Return(x0[2]) →* 656_0_length_Return(x0[3]))∧(x1[2] →* x1[3])∧(x3[2] →* x3[3])∧(x2[2] →* x2[3]))
(3) -> (4), if ((233_0_length_ConstantStackPush(x3[3]) →* 656_0_length_Return(x0[4]))∧(x1[3] →* x1[4])∧(x2[3] →* x2[4])∧(x3[3] →* x3[4]))
(3) -> (16), if ((233_0_length_ConstantStackPush(x3[3]) →* 656_0_length_Return(x0[16]))∧(x1[3] →* x1[16])∧(x2[3] →* x2[16])∧(x3[3] →* java.lang.Object(List(x3[16]))))
(4) -> (5), if ((!(x0[4] % 5 = 0) →* TRUE)∧(656_0_length_Return(x0[4]) →* 656_0_length_Return(x0[5]))∧(x1[4] →* x1[5])∧(x2[4] →* x2[5])∧(x3[4] →* x3[5]))
(5) -> (6), if ((233_0_length_ConstantStackPush(x1[5]) →* 656_0_length_Return(x0[6]))∧(x2[5] →* x2[6])∧(x3[5] →* x3[6])∧(x1[5] →* x1[6]))
(6) -> (7), if ((233_0_length_ConstantStackPush(x2[6]) →* 656_0_length_Return(x0[7]))∧(x1[6] →* x1[7])∧(x3[6] →* x3[7])∧(x0[6] →* x4[7])∧(x2[6] →* x2[7]))
(6) -> (14), if ((233_0_length_ConstantStackPush(x2[6]) →* 656_0_length_Return(x0[14]))∧(x1[6] →* java.lang.Object(List(x1[14])))∧(x3[6] →* x3[14])∧(x0[6] →* x4[14])∧(x2[6] →* x2[14]))
(7) -> (8), if ((x4[7] <= x0[7] →* TRUE)∧(656_0_length_Return(x0[7]) →* 656_0_length_Return(x0[8]))∧(x1[7] →* x1[8])∧(x3[7] →* x3[8])∧(x4[7] →* x4[8])∧(x2[7] →* x2[8]))
(8) -> (9), if ((233_0_length_ConstantStackPush(x1[8]) →* 656_0_length_Return(x0[9]))∧(x2[8] →* x2[9])∧(x3[8] →* x3[9])∧(x1[8] →* x1[9]))
(9) -> (10), if ((233_0_length_ConstantStackPush(x2[9]) →* 656_0_length_Return(x0[10]))∧(x1[9] →* x1[10])∧(x3[9] →* java.lang.Object(List(x3[10])))∧(x0[9] →* x4[10])∧(x2[9] →* x2[10]))
(9) -> (13), if ((233_0_length_ConstantStackPush(x2[9]) →* 656_0_length_Return(x0[13]))∧(x1[9] →* x1[13])∧(x3[9] →* x3[13])∧(x0[9] →* x0[13])∧(x2[9] →* java.lang.Object(List(x2[13]))))
(10) -> (11), if ((!(x4[10] = x0[10]) →* TRUE)∧(656_0_length_Return(x0[10]) →* 656_0_length_Return(x0[11]))∧(x1[10] →* x1[11])∧(java.lang.Object(List(x3[10])) →* java.lang.Object(List(x3[11])))∧(x4[10] →* x4[11])∧(x2[10] →* x2[11]))
(11) -> (12), if ((1100_0_test_Load(x1[11], x2[11], x3[11]) →* 2429_0_test_Return)∧(x1[11] →* x0[12])∧(x2[11] →* x1[12])∧(x3[11] →* x2[12]))
(12) -> (0), if ((233_0_length_ConstantStackPush(x0[12]) →* 656_0_length_Return(x0[0]))∧(x1[12] →* x2[0])∧(x2[12] →* x3[0])∧(x0[12] →* x1[0]))
(13) -> (12), if ((1100_0_test_Load(x1[13], x2[13], x3[13]) →* 2429_0_test_Return)∧(x1[13] →* x0[12])∧(x2[13] →* x1[12])∧(x3[13] →* x2[12]))
(14) -> (15), if ((x4[14] > x0[14] →* TRUE)∧(656_0_length_Return(x0[14]) →* 656_0_length_Return(x0[15]))∧(java.lang.Object(List(x1[14])) →* java.lang.Object(List(x1[15])))∧(x3[14] →* x3[15])∧(x4[14] →* x4[15])∧(x2[14] →* x2[15]))
(15) -> (12), if ((1100_0_test_Load(x1[15], x2[15], x3[15]) →* 2429_0_test_Return)∧(x1[15] →* x0[12])∧(x2[15] →* x1[12])∧(x3[15] →* x2[12]))
(16) -> (17), if ((0 = x0[16] % 5 →* TRUE)∧(656_0_length_Return(x0[16]) →* 656_0_length_Return(x0[17]))∧(x1[16] →* x1[17])∧(x2[16] →* x2[17])∧(java.lang.Object(List(x3[16])) →* java.lang.Object(List(x3[17]))))
(17) -> (6), if ((233_0_length_ConstantStackPush(x1[17]) →* 656_0_length_Return(x0[6]))∧(x2[17] →* x2[6])∧(x3[17] →* x3[6])∧(x1[17] →* x1[6]))
(18) -> (19), if ((0 = x0[18] % 3 →* TRUE)∧(656_0_length_Return(x0[18]) →* 656_0_length_Return(x0[19]))∧(x1[18] →* x1[19])∧(java.lang.Object(List(x3[18])) →* java.lang.Object(List(x3[19])))∧(x2[18] →* x2[19]))
(19) -> (4), if ((233_0_length_ConstantStackPush(java.lang.Object(List(x3[19]))) →* 656_0_length_Return(x0[4]))∧(x1[19] →* x1[4])∧(x2[19] →* x2[4])∧(java.lang.Object(List(x3[19])) →* x3[4]))
(19) -> (16), if ((233_0_length_ConstantStackPush(java.lang.Object(List(x3[19]))) →* 656_0_length_Return(x0[16]))∧(x1[19] →* x1[16])∧(x2[19] →* x2[16])∧(java.lang.Object(List(x3[19])) →* java.lang.Object(List(x3[16]))))
(1) (>(x0[0], 0)=TRUE∧656_0_length_Return(x0[0])=656_0_length_Return(x0[1])∧x2[0]=x2[1]∧x3[0]=x3[1]∧x1[0]=x1[1] ⇒ 233_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[0]), x2[0], x3[0], x1[0])≥NonInfC∧233_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[0]), x2[0], x3[0], x1[0])≥COND_233_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 656_0_length_Return(x0[0]), x2[0], x3[0], x1[0])∧(UIncreasing(COND_233_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 656_0_length_Return(x0[0]), x2[0], x3[0], x1[0])), ≥))
(2) (>(x0[0], 0)=TRUE ⇒ 233_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[0]), x2[0], x3[0], x1[0])≥NonInfC∧233_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[0]), x2[0], x3[0], x1[0])≥COND_233_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 656_0_length_Return(x0[0]), x2[0], x3[0], x1[0])∧(UIncreasing(COND_233_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 656_0_length_Return(x0[0]), x2[0], x3[0], x1[0])), ≥))
(3) (0 ≥ 0 ⇒ (UIncreasing(COND_233_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 656_0_length_Return(x0[0]), x2[0], x3[0], x1[0])), ≥)∧[(-1)bni_123 + (-1)Bound*bni_123] + [bni_123]x1[0] + [bni_123]x3[0] + [bni_123]x2[0] ≥ 0∧[(-1)bso_124] ≥ 0)
(4) (0 ≥ 0 ⇒ (UIncreasing(COND_233_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 656_0_length_Return(x0[0]), x2[0], x3[0], x1[0])), ≥)∧[(-1)bni_123 + (-1)Bound*bni_123] + [bni_123]x1[0] + [bni_123]x3[0] + [bni_123]x2[0] ≥ 0∧[(-1)bso_124] ≥ 0)
(5) (0 ≥ 0 ⇒ (UIncreasing(COND_233_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 656_0_length_Return(x0[0]), x2[0], x3[0], x1[0])), ≥)∧[(-1)bni_123 + (-1)Bound*bni_123] + [bni_123]x1[0] + [bni_123]x3[0] + [bni_123]x2[0] ≥ 0∧[(-1)bso_124] ≥ 0)
(6) (0 ≥ 0 ⇒ (UIncreasing(COND_233_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 656_0_length_Return(x0[0]), x2[0], x3[0], x1[0])), ≥)∧[bni_123] ≥ 0∧[bni_123] ≥ 0∧[bni_123] ≥ 0∧0 ≥ 0∧[(-1)bni_123 + (-1)Bound*bni_123] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_124] ≥ 0)
(7) (>(x0[0], 0)=TRUE∧656_0_length_Return(x0[0])=656_0_length_Return(x0[1])∧x2[0]=x2[1]∧x3[0]=x3[1]∧x1[0]=x1[1]∧233_0_length_ConstantStackPush(x3[1])=656_0_length_Return(x0[2])∧x2[1]=x1[2]∧x1[1]=x3[2]∧x3[1]=x2[2] ⇒ COND_233_1_MAIN_INVOKEMETHOD(TRUE, 656_0_length_Return(x0[1]), x2[1], x3[1], x1[1])≥NonInfC∧COND_233_1_MAIN_INVOKEMETHOD(TRUE, 656_0_length_Return(x0[1]), x2[1], x3[1], x1[1])≥668_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x3[1]), x2[1], x1[1], x3[1])∧(UIncreasing(668_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x3[1]), x2[1], x1[1], x3[1])), ≥))
(8) (>(x0[0], 0)=TRUE∧627_0_length_NULL(0, x3[1])=656_0_length_Return(x0[2]) ⇒ COND_233_1_MAIN_INVOKEMETHOD(TRUE, 656_0_length_Return(x0[0]), x2[0], x3[1], x1[0])≥NonInfC∧COND_233_1_MAIN_INVOKEMETHOD(TRUE, 656_0_length_Return(x0[0]), x2[0], x3[1], x1[0])≥668_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x3[1]), x2[0], x1[0], x3[1])∧(UIncreasing(668_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x3[1]), x2[1], x1[1], x3[1])), ≥))
(9) (0 ≥ 0 ⇒ (UIncreasing(668_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x3[1]), x2[1], x1[1], x3[1])), ≥)∧[(-1)bni_125 + (-1)Bound*bni_125] + [bni_125]x1[0] + [bni_125]x3[1] + [bni_125]x2[0] ≥ 0∧[(-1)bso_126] ≥ 0)
(10) (0 ≥ 0 ⇒ (UIncreasing(668_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x3[1]), x2[1], x1[1], x3[1])), ≥)∧[(-1)bni_125 + (-1)Bound*bni_125] + [bni_125]x1[0] + [bni_125]x3[1] + [bni_125]x2[0] ≥ 0∧[(-1)bso_126] ≥ 0)
(11) (0 ≥ 0 ⇒ (UIncreasing(668_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x3[1]), x2[1], x1[1], x3[1])), ≥)∧[(-1)bni_125 + (-1)Bound*bni_125] + [bni_125]x1[0] + [bni_125]x3[1] + [bni_125]x2[0] ≥ 0∧[(-1)bso_126] ≥ 0)
(12) (0 ≥ 0 ⇒ (UIncreasing(668_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x3[1]), x2[1], x1[1], x3[1])), ≥)∧[bni_125] ≥ 0∧[bni_125] ≥ 0∧[bni_125] ≥ 0∧0 ≥ 0∧[(-1)bni_125 + (-1)Bound*bni_125] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_126] ≥ 0)
(13) (>(x0[0], 0)=TRUE∧656_0_length_Return(x0[0])=656_0_length_Return(x0[1])∧x2[0]=x2[1]∧x3[0]=x3[1]∧x1[0]=x1[1]∧233_0_length_ConstantStackPush(x3[1])=656_0_length_Return(x0[18])∧x2[1]=x1[18]∧x1[1]=java.lang.Object(List(x3[18]))∧x3[1]=x2[18] ⇒ COND_233_1_MAIN_INVOKEMETHOD(TRUE, 656_0_length_Return(x0[1]), x2[1], x3[1], x1[1])≥NonInfC∧COND_233_1_MAIN_INVOKEMETHOD(TRUE, 656_0_length_Return(x0[1]), x2[1], x3[1], x1[1])≥668_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x3[1]), x2[1], x1[1], x3[1])∧(UIncreasing(668_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x3[1]), x2[1], x1[1], x3[1])), ≥))
(14) (>(x0[0], 0)=TRUE∧627_0_length_NULL(0, x3[1])=656_0_length_Return(x0[18]) ⇒ COND_233_1_MAIN_INVOKEMETHOD(TRUE, 656_0_length_Return(x0[0]), x2[0], x3[1], java.lang.Object(List(x3[18])))≥NonInfC∧COND_233_1_MAIN_INVOKEMETHOD(TRUE, 656_0_length_Return(x0[0]), x2[0], x3[1], java.lang.Object(List(x3[18])))≥668_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x3[1]), x2[0], java.lang.Object(List(x3[18])), x3[1])∧(UIncreasing(668_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x3[1]), x2[1], x1[1], x3[1])), ≥))
(15) (0 ≥ 0 ⇒ (UIncreasing(668_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x3[1]), x2[1], x1[1], x3[1])), ≥)∧[(3)bni_125 + (-1)Bound*bni_125] + [(4)bni_125]x3[18] + [bni_125]x3[1] + [bni_125]x2[0] ≥ 0∧[(-1)bso_126] ≥ 0)
(16) (0 ≥ 0 ⇒ (UIncreasing(668_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x3[1]), x2[1], x1[1], x3[1])), ≥)∧[(3)bni_125 + (-1)Bound*bni_125] + [(4)bni_125]x3[18] + [bni_125]x3[1] + [bni_125]x2[0] ≥ 0∧[(-1)bso_126] ≥ 0)
(17) (0 ≥ 0 ⇒ (UIncreasing(668_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x3[1]), x2[1], x1[1], x3[1])), ≥)∧[(3)bni_125 + (-1)Bound*bni_125] + [(4)bni_125]x3[18] + [bni_125]x3[1] + [bni_125]x2[0] ≥ 0∧[(-1)bso_126] ≥ 0)
(18) (0 ≥ 0 ⇒ (UIncreasing(668_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x3[1]), x2[1], x1[1], x3[1])), ≥)∧[(4)bni_125] ≥ 0∧[bni_125] ≥ 0∧[bni_125] ≥ 0∧0 ≥ 0∧[(3)bni_125 + (-1)Bound*bni_125] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_126] ≥ 0)
(19) (!(=(%(x0[2], 3), 0))=TRUE∧656_0_length_Return(x0[2])=656_0_length_Return(x0[3])∧x1[2]=x1[3]∧x3[2]=x3[3]∧x2[2]=x2[3] ⇒ 668_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[2]), x1[2], x3[2], x2[2])≥NonInfC∧668_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[2]), x1[2], x3[2], x2[2])≥COND_668_1_MAIN_INVOKEMETHOD(!(=(%(x0[2], 3), 0)), 656_0_length_Return(x0[2]), x1[2], x3[2], x2[2])∧(UIncreasing(COND_668_1_MAIN_INVOKEMETHOD(!(=(%(x0[2], 3), 0)), 656_0_length_Return(x0[2]), x1[2], x3[2], x2[2])), ≥))
(20) (!(=(%(x0[2], 3), 0))=TRUE ⇒ 668_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[2]), x1[2], x3[2], x2[2])≥NonInfC∧668_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[2]), x1[2], x3[2], x2[2])≥COND_668_1_MAIN_INVOKEMETHOD(!(=(%(x0[2], 3), 0)), 656_0_length_Return(x0[2]), x1[2], x3[2], x2[2])∧(UIncreasing(COND_668_1_MAIN_INVOKEMETHOD(!(=(%(x0[2], 3), 0)), 656_0_length_Return(x0[2]), x1[2], x3[2], x2[2])), ≥))
(21) (0 ≥ 0 ⇒ (UIncreasing(COND_668_1_MAIN_INVOKEMETHOD(!(=(%(x0[2], 3), 0)), 656_0_length_Return(x0[2]), x1[2], x3[2], x2[2])), ≥)∧[(-1)bni_127 + (-1)Bound*bni_127] + [bni_127]x2[2] + [bni_127]x3[2] + [bni_127]x1[2] ≥ 0∧[(-1)bso_128] ≥ 0)
(22) (0 ≥ 0 ⇒ (UIncreasing(COND_668_1_MAIN_INVOKEMETHOD(!(=(%(x0[2], 3), 0)), 656_0_length_Return(x0[2]), x1[2], x3[2], x2[2])), ≥)∧[(-1)bni_127 + (-1)Bound*bni_127] + [bni_127]x2[2] + [bni_127]x3[2] + [bni_127]x1[2] ≥ 0∧[(-1)bso_128] ≥ 0)
(23) (0 ≥ 0 ⇒ (UIncreasing(COND_668_1_MAIN_INVOKEMETHOD(!(=(%(x0[2], 3), 0)), 656_0_length_Return(x0[2]), x1[2], x3[2], x2[2])), ≥)∧[(-1)bni_127 + (-1)Bound*bni_127] + [bni_127]x2[2] + [bni_127]x3[2] + [bni_127]x1[2] ≥ 0∧[(-1)bso_128] ≥ 0)
(24) (0 ≥ 0 ⇒ (UIncreasing(COND_668_1_MAIN_INVOKEMETHOD(!(=(%(x0[2], 3), 0)), 656_0_length_Return(x0[2]), x1[2], x3[2], x2[2])), ≥)∧[bni_127] ≥ 0∧[bni_127] ≥ 0∧[bni_127] ≥ 0∧0 ≥ 0∧[(-1)bni_127 + (-1)Bound*bni_127] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_128] ≥ 0)
(25) (!(=(%(x0[2], 3), 0))=TRUE∧656_0_length_Return(x0[2])=656_0_length_Return(x0[3])∧x1[2]=x1[3]∧x3[2]=x3[3]∧x2[2]=x2[3]∧233_0_length_ConstantStackPush(x3[3])=656_0_length_Return(x0[4])∧x1[3]=x1[4]∧x2[3]=x2[4]∧x3[3]=x3[4] ⇒ COND_668_1_MAIN_INVOKEMETHOD(TRUE, 656_0_length_Return(x0[3]), x1[3], x3[3], x2[3])≥NonInfC∧COND_668_1_MAIN_INVOKEMETHOD(TRUE, 656_0_length_Return(x0[3]), x1[3], x3[3], x2[3])≥718_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x3[3]), x1[3], x2[3], x3[3])∧(UIncreasing(718_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x3[3]), x1[3], x2[3], x3[3])), ≥))
(26) (!(=(%(x0[2], 3), 0))=TRUE∧627_0_length_NULL(0, x3[3])=656_0_length_Return(x0[4]) ⇒ COND_668_1_MAIN_INVOKEMETHOD(TRUE, 656_0_length_Return(x0[2]), x1[2], x3[3], x2[2])≥NonInfC∧COND_668_1_MAIN_INVOKEMETHOD(TRUE, 656_0_length_Return(x0[2]), x1[2], x3[3], x2[2])≥718_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x3[3]), x1[2], x2[2], x3[3])∧(UIncreasing(718_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x3[3]), x1[3], x2[3], x3[3])), ≥))
(27) (0 ≥ 0 ⇒ (UIncreasing(718_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x3[3]), x1[3], x2[3], x3[3])), ≥)∧[(-1)bni_129 + (-1)Bound*bni_129] + [bni_129]x2[2] + [bni_129]x3[3] + [bni_129]x1[2] ≥ 0∧[(-1)bso_130] ≥ 0)
(28) (0 ≥ 0 ⇒ (UIncreasing(718_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x3[3]), x1[3], x2[3], x3[3])), ≥)∧[(-1)bni_129 + (-1)Bound*bni_129] + [bni_129]x2[2] + [bni_129]x3[3] + [bni_129]x1[2] ≥ 0∧[(-1)bso_130] ≥ 0)
(29) (0 ≥ 0 ⇒ (UIncreasing(718_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x3[3]), x1[3], x2[3], x3[3])), ≥)∧[(-1)bni_129 + (-1)Bound*bni_129] + [bni_129]x2[2] + [bni_129]x3[3] + [bni_129]x1[2] ≥ 0∧[(-1)bso_130] ≥ 0)
(30) (0 ≥ 0 ⇒ (UIncreasing(718_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x3[3]), x1[3], x2[3], x3[3])), ≥)∧[bni_129] ≥ 0∧[bni_129] ≥ 0∧[bni_129] ≥ 0∧0 ≥ 0∧[(-1)bni_129 + (-1)Bound*bni_129] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_130] ≥ 0)
(31) (!(=(%(x0[2], 3), 0))=TRUE∧656_0_length_Return(x0[2])=656_0_length_Return(x0[3])∧x1[2]=x1[3]∧x3[2]=x3[3]∧x2[2]=x2[3]∧233_0_length_ConstantStackPush(x3[3])=656_0_length_Return(x0[16])∧x1[3]=x1[16]∧x2[3]=x2[16]∧x3[3]=java.lang.Object(List(x3[16])) ⇒ COND_668_1_MAIN_INVOKEMETHOD(TRUE, 656_0_length_Return(x0[3]), x1[3], x3[3], x2[3])≥NonInfC∧COND_668_1_MAIN_INVOKEMETHOD(TRUE, 656_0_length_Return(x0[3]), x1[3], x3[3], x2[3])≥718_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x3[3]), x1[3], x2[3], x3[3])∧(UIncreasing(718_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x3[3]), x1[3], x2[3], x3[3])), ≥))
(32) (!(=(%(x0[2], 3), 0))=TRUE∧627_0_length_NULL(1, x3[16])=656_0_length_Return(x0[16]) ⇒ COND_668_1_MAIN_INVOKEMETHOD(TRUE, 656_0_length_Return(x0[2]), x1[2], java.lang.Object(List(x3[16])), x2[2])≥NonInfC∧COND_668_1_MAIN_INVOKEMETHOD(TRUE, 656_0_length_Return(x0[2]), x1[2], java.lang.Object(List(x3[16])), x2[2])≥718_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(java.lang.Object(List(x3[16]))), x1[2], x2[2], java.lang.Object(List(x3[16])))∧(UIncreasing(718_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x3[3]), x1[3], x2[3], x3[3])), ≥))
(33) (0 ≥ 0 ⇒ (UIncreasing(718_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x3[3]), x1[3], x2[3], x3[3])), ≥)∧[(3)bni_129 + (-1)Bound*bni_129] + [bni_129]x2[2] + [(4)bni_129]x3[16] + [bni_129]x1[2] ≥ 0∧[(-1)bso_130] ≥ 0)
(34) (0 ≥ 0 ⇒ (UIncreasing(718_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x3[3]), x1[3], x2[3], x3[3])), ≥)∧[(3)bni_129 + (-1)Bound*bni_129] + [bni_129]x2[2] + [(4)bni_129]x3[16] + [bni_129]x1[2] ≥ 0∧[(-1)bso_130] ≥ 0)
(35) (0 ≥ 0 ⇒ (UIncreasing(718_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x3[3]), x1[3], x2[3], x3[3])), ≥)∧[(3)bni_129 + (-1)Bound*bni_129] + [bni_129]x2[2] + [(4)bni_129]x3[16] + [bni_129]x1[2] ≥ 0∧[(-1)bso_130] ≥ 0)
(36) (0 ≥ 0 ⇒ (UIncreasing(718_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x3[3]), x1[3], x2[3], x3[3])), ≥)∧[bni_129] ≥ 0∧[(4)bni_129] ≥ 0∧[bni_129] ≥ 0∧0 ≥ 0∧[(3)bni_129 + (-1)Bound*bni_129] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_130] ≥ 0)
(37) (!(=(%(x0[4], 5), 0))=TRUE∧656_0_length_Return(x0[4])=656_0_length_Return(x0[5])∧x1[4]=x1[5]∧x2[4]=x2[5]∧x3[4]=x3[5] ⇒ 718_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[4]), x1[4], x2[4], x3[4])≥NonInfC∧718_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[4]), x1[4], x2[4], x3[4])≥COND_718_1_MAIN_INVOKEMETHOD(!(=(%(x0[4], 5), 0)), 656_0_length_Return(x0[4]), x1[4], x2[4], x3[4])∧(UIncreasing(COND_718_1_MAIN_INVOKEMETHOD(!(=(%(x0[4], 5), 0)), 656_0_length_Return(x0[4]), x1[4], x2[4], x3[4])), ≥))
(38) (!(=(%(x0[4], 5), 0))=TRUE ⇒ 718_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[4]), x1[4], x2[4], x3[4])≥NonInfC∧718_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[4]), x1[4], x2[4], x3[4])≥COND_718_1_MAIN_INVOKEMETHOD(!(=(%(x0[4], 5), 0)), 656_0_length_Return(x0[4]), x1[4], x2[4], x3[4])∧(UIncreasing(COND_718_1_MAIN_INVOKEMETHOD(!(=(%(x0[4], 5), 0)), 656_0_length_Return(x0[4]), x1[4], x2[4], x3[4])), ≥))
(39) (0 ≥ 0 ⇒ (UIncreasing(COND_718_1_MAIN_INVOKEMETHOD(!(=(%(x0[4], 5), 0)), 656_0_length_Return(x0[4]), x1[4], x2[4], x3[4])), ≥)∧[(-1)bni_131 + (-1)Bound*bni_131] + [bni_131]x3[4] + [bni_131]x2[4] + [bni_131]x1[4] ≥ 0∧[(-1)bso_132] ≥ 0)
(40) (0 ≥ 0 ⇒ (UIncreasing(COND_718_1_MAIN_INVOKEMETHOD(!(=(%(x0[4], 5), 0)), 656_0_length_Return(x0[4]), x1[4], x2[4], x3[4])), ≥)∧[(-1)bni_131 + (-1)Bound*bni_131] + [bni_131]x3[4] + [bni_131]x2[4] + [bni_131]x1[4] ≥ 0∧[(-1)bso_132] ≥ 0)
(41) (0 ≥ 0 ⇒ (UIncreasing(COND_718_1_MAIN_INVOKEMETHOD(!(=(%(x0[4], 5), 0)), 656_0_length_Return(x0[4]), x1[4], x2[4], x3[4])), ≥)∧[(-1)bni_131 + (-1)Bound*bni_131] + [bni_131]x3[4] + [bni_131]x2[4] + [bni_131]x1[4] ≥ 0∧[(-1)bso_132] ≥ 0)
(42) (0 ≥ 0 ⇒ (UIncreasing(COND_718_1_MAIN_INVOKEMETHOD(!(=(%(x0[4], 5), 0)), 656_0_length_Return(x0[4]), x1[4], x2[4], x3[4])), ≥)∧[bni_131] ≥ 0∧[bni_131] ≥ 0∧[bni_131] ≥ 0∧0 ≥ 0∧[(-1)bni_131 + (-1)Bound*bni_131] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_132] ≥ 0)
(43) (!(=(%(x0[4], 5), 0))=TRUE∧656_0_length_Return(x0[4])=656_0_length_Return(x0[5])∧x1[4]=x1[5]∧x2[4]=x2[5]∧x3[4]=x3[5]∧233_0_length_ConstantStackPush(x1[5])=656_0_length_Return(x0[6])∧x2[5]=x2[6]∧x3[5]=x3[6]∧x1[5]=x1[6] ⇒ COND_718_1_MAIN_INVOKEMETHOD(TRUE, 656_0_length_Return(x0[5]), x1[5], x2[5], x3[5])≥NonInfC∧COND_718_1_MAIN_INVOKEMETHOD(TRUE, 656_0_length_Return(x0[5]), x1[5], x2[5], x3[5])≥775_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x1[5]), x2[5], x3[5], x1[5])∧(UIncreasing(775_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x1[5]), x2[5], x3[5], x1[5])), ≥))
(44) (!(=(%(x0[4], 5), 0))=TRUE∧627_0_length_NULL(0, x1[5])=656_0_length_Return(x0[6]) ⇒ COND_718_1_MAIN_INVOKEMETHOD(TRUE, 656_0_length_Return(x0[4]), x1[5], x2[4], x3[4])≥NonInfC∧COND_718_1_MAIN_INVOKEMETHOD(TRUE, 656_0_length_Return(x0[4]), x1[5], x2[4], x3[4])≥775_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x1[5]), x2[4], x3[4], x1[5])∧(UIncreasing(775_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x1[5]), x2[5], x3[5], x1[5])), ≥))
(45) (0 ≥ 0 ⇒ (UIncreasing(775_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x1[5]), x2[5], x3[5], x1[5])), ≥)∧[(-1)bni_133 + (-1)Bound*bni_133] + [bni_133]x3[4] + [bni_133]x2[4] + [bni_133]x1[5] ≥ 0∧[(-1)bso_134] ≥ 0)
(46) (0 ≥ 0 ⇒ (UIncreasing(775_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x1[5]), x2[5], x3[5], x1[5])), ≥)∧[(-1)bni_133 + (-1)Bound*bni_133] + [bni_133]x3[4] + [bni_133]x2[4] + [bni_133]x1[5] ≥ 0∧[(-1)bso_134] ≥ 0)
(47) (0 ≥ 0 ⇒ (UIncreasing(775_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x1[5]), x2[5], x3[5], x1[5])), ≥)∧[(-1)bni_133 + (-1)Bound*bni_133] + [bni_133]x3[4] + [bni_133]x2[4] + [bni_133]x1[5] ≥ 0∧[(-1)bso_134] ≥ 0)
(48) (0 ≥ 0 ⇒ (UIncreasing(775_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x1[5]), x2[5], x3[5], x1[5])), ≥)∧[bni_133] ≥ 0∧[bni_133] ≥ 0∧[bni_133] ≥ 0∧0 ≥ 0∧[(-1)bni_133 + (-1)Bound*bni_133] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_134] ≥ 0)
(49) (233_0_length_ConstantStackPush(x1[5])=656_0_length_Return(x0[6])∧x2[5]=x2[6]∧x3[5]=x3[6]∧x1[5]=x1[6]∧233_0_length_ConstantStackPush(x2[6])=656_0_length_Return(x0[7])∧x1[6]=x1[7]∧x3[6]=x3[7]∧x0[6]=x4[7]∧x2[6]=x2[7] ⇒ 775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), x2[6], x3[6], x1[6])≥NonInfC∧775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), x2[6], x3[6], x1[6])≥807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])∧(UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥))
(50) (0=x0∧627_0_length_NULL(x0, x1[5])=656_0_length_Return(x0[6])∧0=x1∧627_0_length_NULL(x1, x2[6])=656_0_length_Return(x0[7]) ⇒ 775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), x2[6], x3[5], x1[5])≥NonInfC∧775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), x2[6], x3[5], x1[5])≥807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[5], x3[5], x0[6], x2[6])∧(UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥))
(51) (656_0_length_Return(x2)=656_0_length_Return(x0[6])∧0=x2∧0=x1∧627_0_length_NULL(x1, x2[6])=656_0_length_Return(x0[7]) ⇒ 775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), x2[6], x3[5], NULL)≥NonInfC∧775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), x2[6], x3[5], NULL)≥807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), NULL, x3[5], x0[6], x2[6])∧(UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥))
(52) (Cond_627_0_length_NULL(>=(x4, 0), x4, java.lang.Object(List(x3)))=656_0_length_Return(x0[6])∧0=x4∧0=x1∧627_0_length_NULL(x1, x2[6])=656_0_length_Return(x0[7]) ⇒ 775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), x2[6], x3[5], java.lang.Object(List(x3)))≥NonInfC∧775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), x2[6], x3[5], java.lang.Object(List(x3)))≥807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), java.lang.Object(List(x3)), x3[5], x0[6], x2[6])∧(UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥))
(53) (0=x1∧627_0_length_NULL(x1, x2[6])=656_0_length_Return(x0[7]) ⇒ 775_1_MAIN_INVOKEMETHOD(656_0_length_Return(0), x2[6], x3[5], NULL)≥NonInfC∧775_1_MAIN_INVOKEMETHOD(656_0_length_Return(0), x2[6], x3[5], NULL)≥807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), NULL, x3[5], 0, x2[6])∧(UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥))
(54) (>=(x4, 0)=x10∧java.lang.Object(List(x3))=x11∧Cond_627_0_length_NULL(x10, x4, x11)=656_0_length_Return(x0[6])∧0=x4∧0=x1∧627_0_length_NULL(x1, x2[6])=656_0_length_Return(x0[7]) ⇒ 775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), x2[6], x3[5], java.lang.Object(List(x3)))≥NonInfC∧775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), x2[6], x3[5], java.lang.Object(List(x3)))≥807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), java.lang.Object(List(x3)), x3[5], x0[6], x2[6])∧(UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥))
(55) (656_0_length_Return(x5)=656_0_length_Return(x0[7])∧0=x5 ⇒ 775_1_MAIN_INVOKEMETHOD(656_0_length_Return(0), NULL, x3[5], NULL)≥NonInfC∧775_1_MAIN_INVOKEMETHOD(656_0_length_Return(0), NULL, x3[5], NULL)≥807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(NULL), NULL, x3[5], 0, NULL)∧(UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥))
(56) (Cond_627_0_length_NULL(>=(x7, 0), x7, java.lang.Object(List(x6)))=656_0_length_Return(x0[7])∧0=x7 ⇒ 775_1_MAIN_INVOKEMETHOD(656_0_length_Return(0), java.lang.Object(List(x6)), x3[5], NULL)≥NonInfC∧775_1_MAIN_INVOKEMETHOD(656_0_length_Return(0), java.lang.Object(List(x6)), x3[5], NULL)≥807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(java.lang.Object(List(x6))), NULL, x3[5], 0, java.lang.Object(List(x6)))∧(UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥))
(57) (775_1_MAIN_INVOKEMETHOD(656_0_length_Return(0), NULL, x3[5], NULL)≥NonInfC∧775_1_MAIN_INVOKEMETHOD(656_0_length_Return(0), NULL, x3[5], NULL)≥807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(NULL), NULL, x3[5], 0, NULL)∧(UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥))
(58) (Cond_627_0_length_NULL(TRUE, 0, java.lang.Object(List(x6)))=656_0_length_Return(x0[7]) ⇒ 775_1_MAIN_INVOKEMETHOD(656_0_length_Return(0), java.lang.Object(List(x6)), x3[5], NULL)≥NonInfC∧775_1_MAIN_INVOKEMETHOD(656_0_length_Return(0), java.lang.Object(List(x6)), x3[5], NULL)≥807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(java.lang.Object(List(x6))), NULL, x3[5], 0, java.lang.Object(List(x6)))∧(UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥))
(59) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧[(-1)bso_136] ≥ 0)
(60) (656_0_length_Return(x12)=656_0_length_Return(x0[7])∧>=(x4, 0)=x10∧java.lang.Object(List(x3))=x11∧Cond_627_0_length_NULL(x10, x4, x11)=656_0_length_Return(x0[6])∧0=x4∧0=x12 ⇒ 775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), NULL, x3[5], java.lang.Object(List(x3)))≥NonInfC∧775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), NULL, x3[5], java.lang.Object(List(x3)))≥807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(NULL), java.lang.Object(List(x3)), x3[5], x0[6], NULL)∧(UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥))
(61) (Cond_627_0_length_NULL(>=(x14, 0), x14, java.lang.Object(List(x13)))=656_0_length_Return(x0[7])∧>=(x4, 0)=x10∧java.lang.Object(List(x3))=x11∧Cond_627_0_length_NULL(x10, x4, x11)=656_0_length_Return(x0[6])∧0=x4∧0=x14 ⇒ 775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), java.lang.Object(List(x13)), x3[5], java.lang.Object(List(x3)))≥NonInfC∧775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), java.lang.Object(List(x13)), x3[5], java.lang.Object(List(x3)))≥807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(java.lang.Object(List(x13))), java.lang.Object(List(x3)), x3[5], x0[6], java.lang.Object(List(x13)))∧(UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥))
(62) (Cond_627_0_length_NULL(TRUE, 0, java.lang.Object(List(x3)))=656_0_length_Return(x0[6]) ⇒ 775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), NULL, x3[5], java.lang.Object(List(x3)))≥NonInfC∧775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), NULL, x3[5], java.lang.Object(List(x3)))≥807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(NULL), java.lang.Object(List(x3)), x3[5], x0[6], NULL)∧(UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥))
(63) (Cond_627_0_length_NULL(TRUE, 0, java.lang.Object(List(x3)))=656_0_length_Return(x0[6])∧Cond_627_0_length_NULL(TRUE, 0, java.lang.Object(List(x13)))=656_0_length_Return(x0[7]) ⇒ 775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), java.lang.Object(List(x13)), x3[5], java.lang.Object(List(x3)))≥NonInfC∧775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), java.lang.Object(List(x13)), x3[5], java.lang.Object(List(x3)))≥807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(java.lang.Object(List(x13))), java.lang.Object(List(x3)), x3[5], x0[6], java.lang.Object(List(x13)))∧(UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥))
(64) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧0 ≥ 0∧[(-1)bso_136] ≥ 0)
(65) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧0 ≥ 0∧[(-1)bso_136] ≥ 0)
(66) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧0 ≥ 0∧[(-1)bso_136] ≥ 0)
(67) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧[(-1)bso_136] ≥ 0)
(68) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧0 ≥ 0∧[(-1)bso_136] ≥ 0)
(69) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧0 ≥ 0∧[(-1)bso_136] ≥ 0)
(70) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧0 ≥ 0∧[(-1)bso_136] ≥ 0)
(71) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧[(-1)bso_136] ≥ 0)
(72) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧0 ≥ 0∧[(-1)bso_136] ≥ 0)
(73) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧0 ≥ 0∧[(-1)bso_136] ≥ 0)
(74) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧0 ≥ 0∧[(-1)bso_136] ≥ 0)
(75) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧0 ≥ 0∧[(-1)bso_136] ≥ 0)
(76) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_136] ≥ 0)
(77) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_136] ≥ 0)
(78) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_136] ≥ 0)
(79) (233_0_length_ConstantStackPush(x1[17])=656_0_length_Return(x0[6])∧x2[17]=x2[6]∧x3[17]=x3[6]∧x1[17]=x1[6]∧233_0_length_ConstantStackPush(x2[6])=656_0_length_Return(x0[7])∧x1[6]=x1[7]∧x3[6]=x3[7]∧x0[6]=x4[7]∧x2[6]=x2[7] ⇒ 775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), x2[6], x3[6], x1[6])≥NonInfC∧775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), x2[6], x3[6], x1[6])≥807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])∧(UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥))
(80) (0=x17∧627_0_length_NULL(x17, x1[17])=656_0_length_Return(x0[6])∧0=x18∧627_0_length_NULL(x18, x2[6])=656_0_length_Return(x0[7]) ⇒ 775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), x2[6], x3[17], x1[17])≥NonInfC∧775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), x2[6], x3[17], x1[17])≥807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[17], x3[17], x0[6], x2[6])∧(UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥))
(81) (656_0_length_Return(x19)=656_0_length_Return(x0[6])∧0=x19∧0=x18∧627_0_length_NULL(x18, x2[6])=656_0_length_Return(x0[7]) ⇒ 775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), x2[6], x3[17], NULL)≥NonInfC∧775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), x2[6], x3[17], NULL)≥807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), NULL, x3[17], x0[6], x2[6])∧(UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥))
(82) (Cond_627_0_length_NULL(>=(x21, 0), x21, java.lang.Object(List(x20)))=656_0_length_Return(x0[6])∧0=x21∧0=x18∧627_0_length_NULL(x18, x2[6])=656_0_length_Return(x0[7]) ⇒ 775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), x2[6], x3[17], java.lang.Object(List(x20)))≥NonInfC∧775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), x2[6], x3[17], java.lang.Object(List(x20)))≥807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), java.lang.Object(List(x20)), x3[17], x0[6], x2[6])∧(UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥))
(83) (0=x18∧627_0_length_NULL(x18, x2[6])=656_0_length_Return(x0[7]) ⇒ 775_1_MAIN_INVOKEMETHOD(656_0_length_Return(0), x2[6], x3[17], NULL)≥NonInfC∧775_1_MAIN_INVOKEMETHOD(656_0_length_Return(0), x2[6], x3[17], NULL)≥807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), NULL, x3[17], 0, x2[6])∧(UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥))
(84) (>=(x21, 0)=x27∧java.lang.Object(List(x20))=x28∧Cond_627_0_length_NULL(x27, x21, x28)=656_0_length_Return(x0[6])∧0=x21∧0=x18∧627_0_length_NULL(x18, x2[6])=656_0_length_Return(x0[7]) ⇒ 775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), x2[6], x3[17], java.lang.Object(List(x20)))≥NonInfC∧775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), x2[6], x3[17], java.lang.Object(List(x20)))≥807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), java.lang.Object(List(x20)), x3[17], x0[6], x2[6])∧(UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥))
(85) (656_0_length_Return(x22)=656_0_length_Return(x0[7])∧0=x22 ⇒ 775_1_MAIN_INVOKEMETHOD(656_0_length_Return(0), NULL, x3[17], NULL)≥NonInfC∧775_1_MAIN_INVOKEMETHOD(656_0_length_Return(0), NULL, x3[17], NULL)≥807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(NULL), NULL, x3[17], 0, NULL)∧(UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥))
(86) (Cond_627_0_length_NULL(>=(x24, 0), x24, java.lang.Object(List(x23)))=656_0_length_Return(x0[7])∧0=x24 ⇒ 775_1_MAIN_INVOKEMETHOD(656_0_length_Return(0), java.lang.Object(List(x23)), x3[17], NULL)≥NonInfC∧775_1_MAIN_INVOKEMETHOD(656_0_length_Return(0), java.lang.Object(List(x23)), x3[17], NULL)≥807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(java.lang.Object(List(x23))), NULL, x3[17], 0, java.lang.Object(List(x23)))∧(UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥))
(87) (775_1_MAIN_INVOKEMETHOD(656_0_length_Return(0), NULL, x3[17], NULL)≥NonInfC∧775_1_MAIN_INVOKEMETHOD(656_0_length_Return(0), NULL, x3[17], NULL)≥807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(NULL), NULL, x3[17], 0, NULL)∧(UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥))
(88) (Cond_627_0_length_NULL(TRUE, 0, java.lang.Object(List(x23)))=656_0_length_Return(x0[7]) ⇒ 775_1_MAIN_INVOKEMETHOD(656_0_length_Return(0), java.lang.Object(List(x23)), x3[17], NULL)≥NonInfC∧775_1_MAIN_INVOKEMETHOD(656_0_length_Return(0), java.lang.Object(List(x23)), x3[17], NULL)≥807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(java.lang.Object(List(x23))), NULL, x3[17], 0, java.lang.Object(List(x23)))∧(UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥))
(89) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧[(-1)bso_136] ≥ 0)
(90) (656_0_length_Return(x29)=656_0_length_Return(x0[7])∧>=(x21, 0)=x27∧java.lang.Object(List(x20))=x28∧Cond_627_0_length_NULL(x27, x21, x28)=656_0_length_Return(x0[6])∧0=x21∧0=x29 ⇒ 775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), NULL, x3[17], java.lang.Object(List(x20)))≥NonInfC∧775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), NULL, x3[17], java.lang.Object(List(x20)))≥807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(NULL), java.lang.Object(List(x20)), x3[17], x0[6], NULL)∧(UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥))
(91) (Cond_627_0_length_NULL(>=(x31, 0), x31, java.lang.Object(List(x30)))=656_0_length_Return(x0[7])∧>=(x21, 0)=x27∧java.lang.Object(List(x20))=x28∧Cond_627_0_length_NULL(x27, x21, x28)=656_0_length_Return(x0[6])∧0=x21∧0=x31 ⇒ 775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), java.lang.Object(List(x30)), x3[17], java.lang.Object(List(x20)))≥NonInfC∧775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), java.lang.Object(List(x30)), x3[17], java.lang.Object(List(x20)))≥807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(java.lang.Object(List(x30))), java.lang.Object(List(x20)), x3[17], x0[6], java.lang.Object(List(x30)))∧(UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥))
(92) (Cond_627_0_length_NULL(TRUE, 0, java.lang.Object(List(x20)))=656_0_length_Return(x0[6]) ⇒ 775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), NULL, x3[17], java.lang.Object(List(x20)))≥NonInfC∧775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), NULL, x3[17], java.lang.Object(List(x20)))≥807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(NULL), java.lang.Object(List(x20)), x3[17], x0[6], NULL)∧(UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥))
(93) (Cond_627_0_length_NULL(TRUE, 0, java.lang.Object(List(x20)))=656_0_length_Return(x0[6])∧Cond_627_0_length_NULL(TRUE, 0, java.lang.Object(List(x30)))=656_0_length_Return(x0[7]) ⇒ 775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), java.lang.Object(List(x30)), x3[17], java.lang.Object(List(x20)))≥NonInfC∧775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), java.lang.Object(List(x30)), x3[17], java.lang.Object(List(x20)))≥807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(java.lang.Object(List(x30))), java.lang.Object(List(x20)), x3[17], x0[6], java.lang.Object(List(x30)))∧(UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥))
(94) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧0 ≥ 0∧[(-1)bso_136] ≥ 0)
(95) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧0 ≥ 0∧[(-1)bso_136] ≥ 0)
(96) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧0 ≥ 0∧[(-1)bso_136] ≥ 0)
(97) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧[(-1)bso_136] ≥ 0)
(98) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧0 ≥ 0∧[(-1)bso_136] ≥ 0)
(99) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧0 ≥ 0∧[(-1)bso_136] ≥ 0)
(100) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧0 ≥ 0∧[(-1)bso_136] ≥ 0)
(101) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧[(-1)bso_136] ≥ 0)
(102) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧0 ≥ 0∧[(-1)bso_136] ≥ 0)
(103) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧0 ≥ 0∧[(-1)bso_136] ≥ 0)
(104) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧0 ≥ 0∧[(-1)bso_136] ≥ 0)
(105) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧0 ≥ 0∧[(-1)bso_136] ≥ 0)
(106) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_136] ≥ 0)
(107) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_136] ≥ 0)
(108) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_136] ≥ 0)
(109) (233_0_length_ConstantStackPush(x1[5])=656_0_length_Return(x0[6])∧x2[5]=x2[6]∧x3[5]=x3[6]∧x1[5]=x1[6]∧233_0_length_ConstantStackPush(x2[6])=656_0_length_Return(x0[14])∧x1[6]=java.lang.Object(List(x1[14]))∧x3[6]=x3[14]∧x0[6]=x4[14]∧x2[6]=x2[14] ⇒ 775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), x2[6], x3[6], x1[6])≥NonInfC∧775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), x2[6], x3[6], x1[6])≥807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])∧(UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥))
(110) (0=x34∧627_0_length_NULL(x34, x2[6])=656_0_length_Return(x0[14])∧1=x35∧627_0_length_NULL(x35, x1[14])=656_0_length_Return(x0[6]) ⇒ 775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), x2[6], x3[5], java.lang.Object(List(x1[14])))≥NonInfC∧775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), x2[6], x3[5], java.lang.Object(List(x1[14])))≥807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), java.lang.Object(List(x1[14])), x3[5], x0[6], x2[6])∧(UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥))
(111) (656_0_length_Return(x36)=656_0_length_Return(x0[14])∧0=x36∧1=x35∧627_0_length_NULL(x35, x1[14])=656_0_length_Return(x0[6]) ⇒ 775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), NULL, x3[5], java.lang.Object(List(x1[14])))≥NonInfC∧775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), NULL, x3[5], java.lang.Object(List(x1[14])))≥807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(NULL), java.lang.Object(List(x1[14])), x3[5], x0[6], NULL)∧(UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥))
(112) (Cond_627_0_length_NULL(>=(x38, 0), x38, java.lang.Object(List(x37)))=656_0_length_Return(x0[14])∧0=x38∧1=x35∧627_0_length_NULL(x35, x1[14])=656_0_length_Return(x0[6]) ⇒ 775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), java.lang.Object(List(x37)), x3[5], java.lang.Object(List(x1[14])))≥NonInfC∧775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), java.lang.Object(List(x37)), x3[5], java.lang.Object(List(x1[14])))≥807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(java.lang.Object(List(x37))), java.lang.Object(List(x1[14])), x3[5], x0[6], java.lang.Object(List(x37)))∧(UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥))
(113) (1=x35∧627_0_length_NULL(x35, x1[14])=656_0_length_Return(x0[6]) ⇒ 775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), NULL, x3[5], java.lang.Object(List(x1[14])))≥NonInfC∧775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), NULL, x3[5], java.lang.Object(List(x1[14])))≥807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(NULL), java.lang.Object(List(x1[14])), x3[5], x0[6], NULL)∧(UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥))
(114) (>=(x38, 0)=x44∧java.lang.Object(List(x37))=x45∧Cond_627_0_length_NULL(x44, x38, x45)=656_0_length_Return(x0[14])∧0=x38∧1=x35∧627_0_length_NULL(x35, x1[14])=656_0_length_Return(x0[6]) ⇒ 775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), java.lang.Object(List(x37)), x3[5], java.lang.Object(List(x1[14])))≥NonInfC∧775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), java.lang.Object(List(x37)), x3[5], java.lang.Object(List(x1[14])))≥807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(java.lang.Object(List(x37))), java.lang.Object(List(x1[14])), x3[5], x0[6], java.lang.Object(List(x37)))∧(UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥))
(115) (656_0_length_Return(x39)=656_0_length_Return(x0[6])∧1=x39 ⇒ 775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), NULL, x3[5], java.lang.Object(List(NULL)))≥NonInfC∧775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), NULL, x3[5], java.lang.Object(List(NULL)))≥807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(NULL), java.lang.Object(List(NULL)), x3[5], x0[6], NULL)∧(UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥))
(116) (Cond_627_0_length_NULL(>=(x41, 0), x41, java.lang.Object(List(x40)))=656_0_length_Return(x0[6])∧1=x41 ⇒ 775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), NULL, x3[5], java.lang.Object(List(java.lang.Object(List(x40)))))≥NonInfC∧775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), NULL, x3[5], java.lang.Object(List(java.lang.Object(List(x40)))))≥807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(NULL), java.lang.Object(List(java.lang.Object(List(x40)))), x3[5], x0[6], NULL)∧(UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥))
(117) (775_1_MAIN_INVOKEMETHOD(656_0_length_Return(1), NULL, x3[5], java.lang.Object(List(NULL)))≥NonInfC∧775_1_MAIN_INVOKEMETHOD(656_0_length_Return(1), NULL, x3[5], java.lang.Object(List(NULL)))≥807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(NULL), java.lang.Object(List(NULL)), x3[5], 1, NULL)∧(UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥))
(118) (Cond_627_0_length_NULL(TRUE, 1, java.lang.Object(List(x40)))=656_0_length_Return(x0[6]) ⇒ 775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), NULL, x3[5], java.lang.Object(List(java.lang.Object(List(x40)))))≥NonInfC∧775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), NULL, x3[5], java.lang.Object(List(java.lang.Object(List(x40)))))≥807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(NULL), java.lang.Object(List(java.lang.Object(List(x40)))), x3[5], x0[6], NULL)∧(UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥))
(119) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧[(-1)bso_136] ≥ 0)
(120) (656_0_length_Return(x46)=656_0_length_Return(x0[6])∧>=(x38, 0)=x44∧java.lang.Object(List(x37))=x45∧Cond_627_0_length_NULL(x44, x38, x45)=656_0_length_Return(x0[14])∧0=x38∧1=x46 ⇒ 775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), java.lang.Object(List(x37)), x3[5], java.lang.Object(List(NULL)))≥NonInfC∧775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), java.lang.Object(List(x37)), x3[5], java.lang.Object(List(NULL)))≥807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(java.lang.Object(List(x37))), java.lang.Object(List(NULL)), x3[5], x0[6], java.lang.Object(List(x37)))∧(UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥))
(121) (Cond_627_0_length_NULL(>=(x48, 0), x48, java.lang.Object(List(x47)))=656_0_length_Return(x0[6])∧>=(x38, 0)=x44∧java.lang.Object(List(x37))=x45∧Cond_627_0_length_NULL(x44, x38, x45)=656_0_length_Return(x0[14])∧0=x38∧1=x48 ⇒ 775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), java.lang.Object(List(x37)), x3[5], java.lang.Object(List(java.lang.Object(List(x47)))))≥NonInfC∧775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), java.lang.Object(List(x37)), x3[5], java.lang.Object(List(java.lang.Object(List(x47)))))≥807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(java.lang.Object(List(x37))), java.lang.Object(List(java.lang.Object(List(x47)))), x3[5], x0[6], java.lang.Object(List(x37)))∧(UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥))
(122) (Cond_627_0_length_NULL(TRUE, 0, java.lang.Object(List(x37)))=656_0_length_Return(x0[14]) ⇒ 775_1_MAIN_INVOKEMETHOD(656_0_length_Return(1), java.lang.Object(List(x37)), x3[5], java.lang.Object(List(NULL)))≥NonInfC∧775_1_MAIN_INVOKEMETHOD(656_0_length_Return(1), java.lang.Object(List(x37)), x3[5], java.lang.Object(List(NULL)))≥807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(java.lang.Object(List(x37))), java.lang.Object(List(NULL)), x3[5], 1, java.lang.Object(List(x37)))∧(UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥))
(123) (Cond_627_0_length_NULL(TRUE, 0, java.lang.Object(List(x37)))=656_0_length_Return(x0[14])∧Cond_627_0_length_NULL(TRUE, 1, java.lang.Object(List(x47)))=656_0_length_Return(x0[6]) ⇒ 775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), java.lang.Object(List(x37)), x3[5], java.lang.Object(List(java.lang.Object(List(x47)))))≥NonInfC∧775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), java.lang.Object(List(x37)), x3[5], java.lang.Object(List(java.lang.Object(List(x47)))))≥807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(java.lang.Object(List(x37))), java.lang.Object(List(java.lang.Object(List(x47)))), x3[5], x0[6], java.lang.Object(List(x37)))∧(UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥))
(124) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧0 ≥ 0∧[(-1)bso_136] ≥ 0)
(125) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧0 ≥ 0∧[(-1)bso_136] ≥ 0)
(126) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧0 ≥ 0∧[(-1)bso_136] ≥ 0)
(127) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧[(-1)bso_136] ≥ 0)
(128) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧0 ≥ 0∧[(-1)bso_136] ≥ 0)
(129) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧0 ≥ 0∧[(-1)bso_136] ≥ 0)
(130) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧0 ≥ 0∧[(-1)bso_136] ≥ 0)
(131) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧[(-1)bso_136] ≥ 0)
(132) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧0 ≥ 0∧[(-1)bso_136] ≥ 0)
(133) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧0 ≥ 0∧[(-1)bso_136] ≥ 0)
(134) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧0 ≥ 0∧[(-1)bso_136] ≥ 0)
(135) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧0 ≥ 0∧[(-1)bso_136] ≥ 0)
(136) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_136] ≥ 0)
(137) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_136] ≥ 0)
(138) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_136] ≥ 0)
(139) (233_0_length_ConstantStackPush(x1[17])=656_0_length_Return(x0[6])∧x2[17]=x2[6]∧x3[17]=x3[6]∧x1[17]=x1[6]∧233_0_length_ConstantStackPush(x2[6])=656_0_length_Return(x0[14])∧x1[6]=java.lang.Object(List(x1[14]))∧x3[6]=x3[14]∧x0[6]=x4[14]∧x2[6]=x2[14] ⇒ 775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), x2[6], x3[6], x1[6])≥NonInfC∧775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), x2[6], x3[6], x1[6])≥807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])∧(UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥))
(140) (0=x51∧627_0_length_NULL(x51, x2[6])=656_0_length_Return(x0[14])∧1=x52∧627_0_length_NULL(x52, x1[14])=656_0_length_Return(x0[6]) ⇒ 775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), x2[6], x3[17], java.lang.Object(List(x1[14])))≥NonInfC∧775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), x2[6], x3[17], java.lang.Object(List(x1[14])))≥807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), java.lang.Object(List(x1[14])), x3[17], x0[6], x2[6])∧(UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥))
(141) (656_0_length_Return(x53)=656_0_length_Return(x0[14])∧0=x53∧1=x52∧627_0_length_NULL(x52, x1[14])=656_0_length_Return(x0[6]) ⇒ 775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), NULL, x3[17], java.lang.Object(List(x1[14])))≥NonInfC∧775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), NULL, x3[17], java.lang.Object(List(x1[14])))≥807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(NULL), java.lang.Object(List(x1[14])), x3[17], x0[6], NULL)∧(UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥))
(142) (Cond_627_0_length_NULL(>=(x55, 0), x55, java.lang.Object(List(x54)))=656_0_length_Return(x0[14])∧0=x55∧1=x52∧627_0_length_NULL(x52, x1[14])=656_0_length_Return(x0[6]) ⇒ 775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), java.lang.Object(List(x54)), x3[17], java.lang.Object(List(x1[14])))≥NonInfC∧775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), java.lang.Object(List(x54)), x3[17], java.lang.Object(List(x1[14])))≥807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(java.lang.Object(List(x54))), java.lang.Object(List(x1[14])), x3[17], x0[6], java.lang.Object(List(x54)))∧(UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥))
(143) (1=x52∧627_0_length_NULL(x52, x1[14])=656_0_length_Return(x0[6]) ⇒ 775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), NULL, x3[17], java.lang.Object(List(x1[14])))≥NonInfC∧775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), NULL, x3[17], java.lang.Object(List(x1[14])))≥807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(NULL), java.lang.Object(List(x1[14])), x3[17], x0[6], NULL)∧(UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥))
(144) (>=(x55, 0)=x61∧java.lang.Object(List(x54))=x62∧Cond_627_0_length_NULL(x61, x55, x62)=656_0_length_Return(x0[14])∧0=x55∧1=x52∧627_0_length_NULL(x52, x1[14])=656_0_length_Return(x0[6]) ⇒ 775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), java.lang.Object(List(x54)), x3[17], java.lang.Object(List(x1[14])))≥NonInfC∧775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), java.lang.Object(List(x54)), x3[17], java.lang.Object(List(x1[14])))≥807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(java.lang.Object(List(x54))), java.lang.Object(List(x1[14])), x3[17], x0[6], java.lang.Object(List(x54)))∧(UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥))
(145) (656_0_length_Return(x56)=656_0_length_Return(x0[6])∧1=x56 ⇒ 775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), NULL, x3[17], java.lang.Object(List(NULL)))≥NonInfC∧775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), NULL, x3[17], java.lang.Object(List(NULL)))≥807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(NULL), java.lang.Object(List(NULL)), x3[17], x0[6], NULL)∧(UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥))
(146) (Cond_627_0_length_NULL(>=(x58, 0), x58, java.lang.Object(List(x57)))=656_0_length_Return(x0[6])∧1=x58 ⇒ 775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), NULL, x3[17], java.lang.Object(List(java.lang.Object(List(x57)))))≥NonInfC∧775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), NULL, x3[17], java.lang.Object(List(java.lang.Object(List(x57)))))≥807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(NULL), java.lang.Object(List(java.lang.Object(List(x57)))), x3[17], x0[6], NULL)∧(UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥))
(147) (775_1_MAIN_INVOKEMETHOD(656_0_length_Return(1), NULL, x3[17], java.lang.Object(List(NULL)))≥NonInfC∧775_1_MAIN_INVOKEMETHOD(656_0_length_Return(1), NULL, x3[17], java.lang.Object(List(NULL)))≥807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(NULL), java.lang.Object(List(NULL)), x3[17], 1, NULL)∧(UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥))
(148) (Cond_627_0_length_NULL(TRUE, 1, java.lang.Object(List(x57)))=656_0_length_Return(x0[6]) ⇒ 775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), NULL, x3[17], java.lang.Object(List(java.lang.Object(List(x57)))))≥NonInfC∧775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), NULL, x3[17], java.lang.Object(List(java.lang.Object(List(x57)))))≥807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(NULL), java.lang.Object(List(java.lang.Object(List(x57)))), x3[17], x0[6], NULL)∧(UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥))
(149) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧[(-1)bso_136] ≥ 0)
(150) (656_0_length_Return(x63)=656_0_length_Return(x0[6])∧>=(x55, 0)=x61∧java.lang.Object(List(x54))=x62∧Cond_627_0_length_NULL(x61, x55, x62)=656_0_length_Return(x0[14])∧0=x55∧1=x63 ⇒ 775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), java.lang.Object(List(x54)), x3[17], java.lang.Object(List(NULL)))≥NonInfC∧775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), java.lang.Object(List(x54)), x3[17], java.lang.Object(List(NULL)))≥807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(java.lang.Object(List(x54))), java.lang.Object(List(NULL)), x3[17], x0[6], java.lang.Object(List(x54)))∧(UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥))
(151) (Cond_627_0_length_NULL(>=(x65, 0), x65, java.lang.Object(List(x64)))=656_0_length_Return(x0[6])∧>=(x55, 0)=x61∧java.lang.Object(List(x54))=x62∧Cond_627_0_length_NULL(x61, x55, x62)=656_0_length_Return(x0[14])∧0=x55∧1=x65 ⇒ 775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), java.lang.Object(List(x54)), x3[17], java.lang.Object(List(java.lang.Object(List(x64)))))≥NonInfC∧775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), java.lang.Object(List(x54)), x3[17], java.lang.Object(List(java.lang.Object(List(x64)))))≥807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(java.lang.Object(List(x54))), java.lang.Object(List(java.lang.Object(List(x64)))), x3[17], x0[6], java.lang.Object(List(x54)))∧(UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥))
(152) (Cond_627_0_length_NULL(TRUE, 0, java.lang.Object(List(x54)))=656_0_length_Return(x0[14]) ⇒ 775_1_MAIN_INVOKEMETHOD(656_0_length_Return(1), java.lang.Object(List(x54)), x3[17], java.lang.Object(List(NULL)))≥NonInfC∧775_1_MAIN_INVOKEMETHOD(656_0_length_Return(1), java.lang.Object(List(x54)), x3[17], java.lang.Object(List(NULL)))≥807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(java.lang.Object(List(x54))), java.lang.Object(List(NULL)), x3[17], 1, java.lang.Object(List(x54)))∧(UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥))
(153) (Cond_627_0_length_NULL(TRUE, 0, java.lang.Object(List(x54)))=656_0_length_Return(x0[14])∧Cond_627_0_length_NULL(TRUE, 1, java.lang.Object(List(x64)))=656_0_length_Return(x0[6]) ⇒ 775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), java.lang.Object(List(x54)), x3[17], java.lang.Object(List(java.lang.Object(List(x64)))))≥NonInfC∧775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), java.lang.Object(List(x54)), x3[17], java.lang.Object(List(java.lang.Object(List(x64)))))≥807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(java.lang.Object(List(x54))), java.lang.Object(List(java.lang.Object(List(x64)))), x3[17], x0[6], java.lang.Object(List(x54)))∧(UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥))
(154) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧0 ≥ 0∧[(-1)bso_136] ≥ 0)
(155) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧0 ≥ 0∧[(-1)bso_136] ≥ 0)
(156) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧0 ≥ 0∧[(-1)bso_136] ≥ 0)
(157) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧[(-1)bso_136] ≥ 0)
(158) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧0 ≥ 0∧[(-1)bso_136] ≥ 0)
(159) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧0 ≥ 0∧[(-1)bso_136] ≥ 0)
(160) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧0 ≥ 0∧[(-1)bso_136] ≥ 0)
(161) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧[(-1)bso_136] ≥ 0)
(162) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧0 ≥ 0∧[(-1)bso_136] ≥ 0)
(163) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧0 ≥ 0∧[(-1)bso_136] ≥ 0)
(164) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧0 ≥ 0∧[(-1)bso_136] ≥ 0)
(165) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧0 ≥ 0∧[(-1)bso_136] ≥ 0)
(166) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_136] ≥ 0)
(167) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_136] ≥ 0)
(168) ((UIncreasing(807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_136] ≥ 0)
(169) (<=(x4[7], x0[7])=TRUE∧656_0_length_Return(x0[7])=656_0_length_Return(x0[8])∧x1[7]=x1[8]∧x3[7]=x3[8]∧x4[7]=x4[8]∧x2[7]=x2[8] ⇒ 807_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[7]), x1[7], x3[7], x4[7], x2[7])≥NonInfC∧807_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[7]), x1[7], x3[7], x4[7], x2[7])≥COND_807_1_MAIN_INVOKEMETHOD(<=(x4[7], x0[7]), 656_0_length_Return(x0[7]), x1[7], x3[7], x4[7], x2[7])∧(UIncreasing(COND_807_1_MAIN_INVOKEMETHOD(<=(x4[7], x0[7]), 656_0_length_Return(x0[7]), x1[7], x3[7], x4[7], x2[7])), ≥))
(170) (<=(x4[7], x0[7])=TRUE ⇒ 807_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[7]), x1[7], x3[7], x4[7], x2[7])≥NonInfC∧807_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[7]), x1[7], x3[7], x4[7], x2[7])≥COND_807_1_MAIN_INVOKEMETHOD(<=(x4[7], x0[7]), 656_0_length_Return(x0[7]), x1[7], x3[7], x4[7], x2[7])∧(UIncreasing(COND_807_1_MAIN_INVOKEMETHOD(<=(x4[7], x0[7]), 656_0_length_Return(x0[7]), x1[7], x3[7], x4[7], x2[7])), ≥))
(171) (0 ≥ 0 ⇒ (UIncreasing(COND_807_1_MAIN_INVOKEMETHOD(<=(x4[7], x0[7]), 656_0_length_Return(x0[7]), x1[7], x3[7], x4[7], x2[7])), ≥)∧[(-1)bni_137 + (-1)Bound*bni_137] + [bni_137]x2[7] + [bni_137]x3[7] + [bni_137]x1[7] ≥ 0∧[(-1)bso_138] ≥ 0)
(172) (0 ≥ 0 ⇒ (UIncreasing(COND_807_1_MAIN_INVOKEMETHOD(<=(x4[7], x0[7]), 656_0_length_Return(x0[7]), x1[7], x3[7], x4[7], x2[7])), ≥)∧[(-1)bni_137 + (-1)Bound*bni_137] + [bni_137]x2[7] + [bni_137]x3[7] + [bni_137]x1[7] ≥ 0∧[(-1)bso_138] ≥ 0)
(173) (0 ≥ 0 ⇒ (UIncreasing(COND_807_1_MAIN_INVOKEMETHOD(<=(x4[7], x0[7]), 656_0_length_Return(x0[7]), x1[7], x3[7], x4[7], x2[7])), ≥)∧[(-1)bni_137 + (-1)Bound*bni_137] + [bni_137]x2[7] + [bni_137]x3[7] + [bni_137]x1[7] ≥ 0∧[(-1)bso_138] ≥ 0)
(174) (0 ≥ 0 ⇒ (UIncreasing(COND_807_1_MAIN_INVOKEMETHOD(<=(x4[7], x0[7]), 656_0_length_Return(x0[7]), x1[7], x3[7], x4[7], x2[7])), ≥)∧[bni_137] ≥ 0∧0 ≥ 0∧[bni_137] ≥ 0∧[bni_137] ≥ 0∧0 ≥ 0∧[(-1)bni_137 + (-1)Bound*bni_137] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_138] ≥ 0)
(175) (<=(x4[7], x0[7])=TRUE∧656_0_length_Return(x0[7])=656_0_length_Return(x0[8])∧x1[7]=x1[8]∧x3[7]=x3[8]∧x4[7]=x4[8]∧x2[7]=x2[8]∧233_0_length_ConstantStackPush(x1[8])=656_0_length_Return(x0[9])∧x2[8]=x2[9]∧x3[8]=x3[9]∧x1[8]=x1[9] ⇒ COND_807_1_MAIN_INVOKEMETHOD(TRUE, 656_0_length_Return(x0[8]), x1[8], x3[8], x4[8], x2[8])≥NonInfC∧COND_807_1_MAIN_INVOKEMETHOD(TRUE, 656_0_length_Return(x0[8]), x1[8], x3[8], x4[8], x2[8])≥867_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x1[8]), x2[8], x3[8], x1[8])∧(UIncreasing(867_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x1[8]), x2[8], x3[8], x1[8])), ≥))
(176) (<=(x4[7], x0[7])=TRUE∧0=x68∧627_0_length_NULL(x68, x1[8])=656_0_length_Return(x0[9]) ⇒ COND_807_1_MAIN_INVOKEMETHOD(TRUE, 656_0_length_Return(x0[7]), x1[8], x3[7], x4[7], x2[7])≥NonInfC∧COND_807_1_MAIN_INVOKEMETHOD(TRUE, 656_0_length_Return(x0[7]), x1[8], x3[7], x4[7], x2[7])≥867_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x1[8]), x2[7], x3[7], x1[8])∧(UIncreasing(867_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x1[8]), x2[8], x3[8], x1[8])), ≥))
(177) (656_0_length_Return(x69)=656_0_length_Return(x0[9])∧<=(x4[7], x0[7])=TRUE∧0=x69 ⇒ COND_807_1_MAIN_INVOKEMETHOD(TRUE, 656_0_length_Return(x0[7]), NULL, x3[7], x4[7], x2[7])≥NonInfC∧COND_807_1_MAIN_INVOKEMETHOD(TRUE, 656_0_length_Return(x0[7]), NULL, x3[7], x4[7], x2[7])≥867_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(NULL), x2[7], x3[7], NULL)∧(UIncreasing(867_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x1[8]), x2[8], x3[8], x1[8])), ≥))
(178) (Cond_627_0_length_NULL(>=(x71, 0), x71, java.lang.Object(List(x70)))=656_0_length_Return(x0[9])∧<=(x4[7], x0[7])=TRUE∧0=x71 ⇒ COND_807_1_MAIN_INVOKEMETHOD(TRUE, 656_0_length_Return(x0[7]), java.lang.Object(List(x70)), x3[7], x4[7], x2[7])≥NonInfC∧COND_807_1_MAIN_INVOKEMETHOD(TRUE, 656_0_length_Return(x0[7]), java.lang.Object(List(x70)), x3[7], x4[7], x2[7])≥867_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(java.lang.Object(List(x70))), x2[7], x3[7], java.lang.Object(List(x70)))∧(UIncreasing(867_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x1[8]), x2[8], x3[8], x1[8])), ≥))
(179) (<=(x4[7], x0[7])=TRUE ⇒ COND_807_1_MAIN_INVOKEMETHOD(TRUE, 656_0_length_Return(x0[7]), NULL, x3[7], x4[7], x2[7])≥NonInfC∧COND_807_1_MAIN_INVOKEMETHOD(TRUE, 656_0_length_Return(x0[7]), NULL, x3[7], x4[7], x2[7])≥867_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(NULL), x2[7], x3[7], NULL)∧(UIncreasing(867_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x1[8]), x2[8], x3[8], x1[8])), ≥))
(180) (<=(x4[7], x0[7])=TRUE∧Cond_627_0_length_NULL(TRUE, 0, java.lang.Object(List(x70)))=656_0_length_Return(x0[9]) ⇒ COND_807_1_MAIN_INVOKEMETHOD(TRUE, 656_0_length_Return(x0[7]), java.lang.Object(List(x70)), x3[7], x4[7], x2[7])≥NonInfC∧COND_807_1_MAIN_INVOKEMETHOD(TRUE, 656_0_length_Return(x0[7]), java.lang.Object(List(x70)), x3[7], x4[7], x2[7])≥867_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(java.lang.Object(List(x70))), x2[7], x3[7], java.lang.Object(List(x70)))∧(UIncreasing(867_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x1[8]), x2[8], x3[8], x1[8])), ≥))
(181) (0 ≥ 0 ⇒ (UIncreasing(867_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x1[8]), x2[8], x3[8], x1[8])), ≥)∧[(-1)bni_139 + (-1)Bound*bni_139] + [bni_139]x2[7] + [bni_139]x3[7] ≥ 0∧[(-1)bso_140] ≥ 0)
(182) (0 ≥ 0 ⇒ (UIncreasing(867_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x1[8]), x2[8], x3[8], x1[8])), ≥)∧[(3)bni_139 + (-1)Bound*bni_139] + [bni_139]x2[7] + [bni_139]x3[7] + [(4)bni_139]x70 ≥ 0∧[(-1)bso_140] ≥ 0)
(183) (0 ≥ 0 ⇒ (UIncreasing(867_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x1[8]), x2[8], x3[8], x1[8])), ≥)∧[(-1)bni_139 + (-1)Bound*bni_139] + [bni_139]x2[7] + [bni_139]x3[7] ≥ 0∧[(-1)bso_140] ≥ 0)
(184) (0 ≥ 0 ⇒ (UIncreasing(867_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x1[8]), x2[8], x3[8], x1[8])), ≥)∧[(3)bni_139 + (-1)Bound*bni_139] + [bni_139]x2[7] + [bni_139]x3[7] + [(4)bni_139]x70 ≥ 0∧[(-1)bso_140] ≥ 0)
(185) (0 ≥ 0 ⇒ (UIncreasing(867_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x1[8]), x2[8], x3[8], x1[8])), ≥)∧[(-1)bni_139 + (-1)Bound*bni_139] + [bni_139]x2[7] + [bni_139]x3[7] ≥ 0∧[(-1)bso_140] ≥ 0)
(186) (0 ≥ 0 ⇒ (UIncreasing(867_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x1[8]), x2[8], x3[8], x1[8])), ≥)∧[(3)bni_139 + (-1)Bound*bni_139] + [bni_139]x2[7] + [bni_139]x3[7] + [(4)bni_139]x70 ≥ 0∧[(-1)bso_140] ≥ 0)
(187) (0 ≥ 0 ⇒ (UIncreasing(867_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x1[8]), x2[8], x3[8], x1[8])), ≥)∧[bni_139] ≥ 0∧0 ≥ 0∧[bni_139] ≥ 0∧0 ≥ 0∧[(-1)bni_139 + (-1)Bound*bni_139] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_140] ≥ 0)
(188) (0 ≥ 0 ⇒ (UIncreasing(867_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x1[8]), x2[8], x3[8], x1[8])), ≥)∧[bni_139] ≥ 0∧0 ≥ 0∧[bni_139] ≥ 0∧[(4)bni_139] ≥ 0∧0 ≥ 0∧[(3)bni_139 + (-1)Bound*bni_139] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_140] ≥ 0)
(189) (233_0_length_ConstantStackPush(x1[8])=656_0_length_Return(x0[9])∧x2[8]=x2[9]∧x3[8]=x3[9]∧x1[8]=x1[9]∧233_0_length_ConstantStackPush(x2[9])=656_0_length_Return(x0[10])∧x1[9]=x1[10]∧x3[9]=java.lang.Object(List(x3[10]))∧x0[9]=x4[10]∧x2[9]=x2[10] ⇒ 867_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[9]), x2[9], x3[9], x1[9])≥NonInfC∧867_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[9]), x2[9], x3[9], x1[9])≥908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[9]), x1[9], x3[9], x0[9], x2[9])∧(UIncreasing(908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[9]), x1[9], x3[9], x0[9], x2[9])), ≥))
(190) (0=x74∧627_0_length_NULL(x74, x1[8])=656_0_length_Return(x0[9])∧0=x75∧627_0_length_NULL(x75, x2[9])=656_0_length_Return(x0[10]) ⇒ 867_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[9]), x2[9], java.lang.Object(List(x3[10])), x1[8])≥NonInfC∧867_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[9]), x2[9], java.lang.Object(List(x3[10])), x1[8])≥908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[9]), x1[8], java.lang.Object(List(x3[10])), x0[9], x2[9])∧(UIncreasing(908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[9]), x1[9], x3[9], x0[9], x2[9])), ≥))
(191) (656_0_length_Return(x76)=656_0_length_Return(x0[9])∧0=x76∧0=x75∧627_0_length_NULL(x75, x2[9])=656_0_length_Return(x0[10]) ⇒ 867_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[9]), x2[9], java.lang.Object(List(x3[10])), NULL)≥NonInfC∧867_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[9]), x2[9], java.lang.Object(List(x3[10])), NULL)≥908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[9]), NULL, java.lang.Object(List(x3[10])), x0[9], x2[9])∧(UIncreasing(908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[9]), x1[9], x3[9], x0[9], x2[9])), ≥))
(192) (Cond_627_0_length_NULL(>=(x78, 0), x78, java.lang.Object(List(x77)))=656_0_length_Return(x0[9])∧0=x78∧0=x75∧627_0_length_NULL(x75, x2[9])=656_0_length_Return(x0[10]) ⇒ 867_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[9]), x2[9], java.lang.Object(List(x3[10])), java.lang.Object(List(x77)))≥NonInfC∧867_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[9]), x2[9], java.lang.Object(List(x3[10])), java.lang.Object(List(x77)))≥908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[9]), java.lang.Object(List(x77)), java.lang.Object(List(x3[10])), x0[9], x2[9])∧(UIncreasing(908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[9]), x1[9], x3[9], x0[9], x2[9])), ≥))
(193) (0=x75∧627_0_length_NULL(x75, x2[9])=656_0_length_Return(x0[10]) ⇒ 867_1_MAIN_INVOKEMETHOD(656_0_length_Return(0), x2[9], java.lang.Object(List(x3[10])), NULL)≥NonInfC∧867_1_MAIN_INVOKEMETHOD(656_0_length_Return(0), x2[9], java.lang.Object(List(x3[10])), NULL)≥908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[9]), NULL, java.lang.Object(List(x3[10])), 0, x2[9])∧(UIncreasing(908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[9]), x1[9], x3[9], x0[9], x2[9])), ≥))
(194) (>=(x78, 0)=x84∧java.lang.Object(List(x77))=x85∧Cond_627_0_length_NULL(x84, x78, x85)=656_0_length_Return(x0[9])∧0=x78∧0=x75∧627_0_length_NULL(x75, x2[9])=656_0_length_Return(x0[10]) ⇒ 867_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[9]), x2[9], java.lang.Object(List(x3[10])), java.lang.Object(List(x77)))≥NonInfC∧867_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[9]), x2[9], java.lang.Object(List(x3[10])), java.lang.Object(List(x77)))≥908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[9]), java.lang.Object(List(x77)), java.lang.Object(List(x3[10])), x0[9], x2[9])∧(UIncreasing(908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[9]), x1[9], x3[9], x0[9], x2[9])), ≥))
(195) (656_0_length_Return(x79)=656_0_length_Return(x0[10])∧0=x79 ⇒ 867_1_MAIN_INVOKEMETHOD(656_0_length_Return(0), NULL, java.lang.Object(List(x3[10])), NULL)≥NonInfC∧867_1_MAIN_INVOKEMETHOD(656_0_length_Return(0), NULL, java.lang.Object(List(x3[10])), NULL)≥908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(NULL), NULL, java.lang.Object(List(x3[10])), 0, NULL)∧(UIncreasing(908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[9]), x1[9], x3[9], x0[9], x2[9])), ≥))
(196) (Cond_627_0_length_NULL(>=(x81, 0), x81, java.lang.Object(List(x80)))=656_0_length_Return(x0[10])∧0=x81 ⇒ 867_1_MAIN_INVOKEMETHOD(656_0_length_Return(0), java.lang.Object(List(x80)), java.lang.Object(List(x3[10])), NULL)≥NonInfC∧867_1_MAIN_INVOKEMETHOD(656_0_length_Return(0), java.lang.Object(List(x80)), java.lang.Object(List(x3[10])), NULL)≥908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(java.lang.Object(List(x80))), NULL, java.lang.Object(List(x3[10])), 0, java.lang.Object(List(x80)))∧(UIncreasing(908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[9]), x1[9], x3[9], x0[9], x2[9])), ≥))
(197) (867_1_MAIN_INVOKEMETHOD(656_0_length_Return(0), NULL, java.lang.Object(List(x3[10])), NULL)≥NonInfC∧867_1_MAIN_INVOKEMETHOD(656_0_length_Return(0), NULL, java.lang.Object(List(x3[10])), NULL)≥908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(NULL), NULL, java.lang.Object(List(x3[10])), 0, NULL)∧(UIncreasing(908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[9]), x1[9], x3[9], x0[9], x2[9])), ≥))
(198) (Cond_627_0_length_NULL(TRUE, 0, java.lang.Object(List(x80)))=656_0_length_Return(x0[10]) ⇒ 867_1_MAIN_INVOKEMETHOD(656_0_length_Return(0), java.lang.Object(List(x80)), java.lang.Object(List(x3[10])), NULL)≥NonInfC∧867_1_MAIN_INVOKEMETHOD(656_0_length_Return(0), java.lang.Object(List(x80)), java.lang.Object(List(x3[10])), NULL)≥908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(java.lang.Object(List(x80))), NULL, java.lang.Object(List(x3[10])), 0, java.lang.Object(List(x80)))∧(UIncreasing(908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[9]), x1[9], x3[9], x0[9], x2[9])), ≥))
(199) ((UIncreasing(908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[9]), x1[9], x3[9], x0[9], x2[9])), ≥)∧[(-1)bso_142] ≥ 0)
(200) (656_0_length_Return(x86)=656_0_length_Return(x0[10])∧>=(x78, 0)=x84∧java.lang.Object(List(x77))=x85∧Cond_627_0_length_NULL(x84, x78, x85)=656_0_length_Return(x0[9])∧0=x78∧0=x86 ⇒ 867_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[9]), NULL, java.lang.Object(List(x3[10])), java.lang.Object(List(x77)))≥NonInfC∧867_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[9]), NULL, java.lang.Object(List(x3[10])), java.lang.Object(List(x77)))≥908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(NULL), java.lang.Object(List(x77)), java.lang.Object(List(x3[10])), x0[9], NULL)∧(UIncreasing(908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[9]), x1[9], x3[9], x0[9], x2[9])), ≥))
(201) (Cond_627_0_length_NULL(>=(x88, 0), x88, java.lang.Object(List(x87)))=656_0_length_Return(x0[10])∧>=(x78, 0)=x84∧java.lang.Object(List(x77))=x85∧Cond_627_0_length_NULL(x84, x78, x85)=656_0_length_Return(x0[9])∧0=x78∧0=x88 ⇒ 867_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[9]), java.lang.Object(List(x87)), java.lang.Object(List(x3[10])), java.lang.Object(List(x77)))≥NonInfC∧867_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[9]), java.lang.Object(List(x87)), java.lang.Object(List(x3[10])), java.lang.Object(List(x77)))≥908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(java.lang.Object(List(x87))), java.lang.Object(List(x77)), java.lang.Object(List(x3[10])), x0[9], java.lang.Object(List(x87)))∧(UIncreasing(908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[9]), x1[9], x3[9], x0[9], x2[9])), ≥))
(202) (Cond_627_0_length_NULL(TRUE, 0, java.lang.Object(List(x77)))=656_0_length_Return(x0[9]) ⇒ 867_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[9]), NULL, java.lang.Object(List(x3[10])), java.lang.Object(List(x77)))≥NonInfC∧867_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[9]), NULL, java.lang.Object(List(x3[10])), java.lang.Object(List(x77)))≥908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(NULL), java.lang.Object(List(x77)), java.lang.Object(List(x3[10])), x0[9], NULL)∧(UIncreasing(908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[9]), x1[9], x3[9], x0[9], x2[9])), ≥))
(203) (Cond_627_0_length_NULL(TRUE, 0, java.lang.Object(List(x77)))=656_0_length_Return(x0[9])∧Cond_627_0_length_NULL(TRUE, 0, java.lang.Object(List(x87)))=656_0_length_Return(x0[10]) ⇒ 867_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[9]), java.lang.Object(List(x87)), java.lang.Object(List(x3[10])), java.lang.Object(List(x77)))≥NonInfC∧867_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[9]), java.lang.Object(List(x87)), java.lang.Object(List(x3[10])), java.lang.Object(List(x77)))≥908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(java.lang.Object(List(x87))), java.lang.Object(List(x77)), java.lang.Object(List(x3[10])), x0[9], java.lang.Object(List(x87)))∧(UIncreasing(908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[9]), x1[9], x3[9], x0[9], x2[9])), ≥))
(204) ((UIncreasing(908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[9]), x1[9], x3[9], x0[9], x2[9])), ≥)∧0 ≥ 0∧[(-1)bso_142] ≥ 0)
(205) ((UIncreasing(908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[9]), x1[9], x3[9], x0[9], x2[9])), ≥)∧0 ≥ 0∧[(-1)bso_142] ≥ 0)
(206) ((UIncreasing(908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[9]), x1[9], x3[9], x0[9], x2[9])), ≥)∧0 ≥ 0∧[(-1)bso_142] ≥ 0)
(207) ((UIncreasing(908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[9]), x1[9], x3[9], x0[9], x2[9])), ≥)∧[(-1)bso_142] ≥ 0)
(208) ((UIncreasing(908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[9]), x1[9], x3[9], x0[9], x2[9])), ≥)∧0 ≥ 0∧[(-1)bso_142] ≥ 0)
(209) ((UIncreasing(908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[9]), x1[9], x3[9], x0[9], x2[9])), ≥)∧0 ≥ 0∧[(-1)bso_142] ≥ 0)
(210) ((UIncreasing(908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[9]), x1[9], x3[9], x0[9], x2[9])), ≥)∧0 ≥ 0∧[(-1)bso_142] ≥ 0)
(211) ((UIncreasing(908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[9]), x1[9], x3[9], x0[9], x2[9])), ≥)∧[(-1)bso_142] ≥ 0)
(212) ((UIncreasing(908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[9]), x1[9], x3[9], x0[9], x2[9])), ≥)∧0 ≥ 0∧[(-1)bso_142] ≥ 0)
(213) ((UIncreasing(908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[9]), x1[9], x3[9], x0[9], x2[9])), ≥)∧0 ≥ 0∧[(-1)bso_142] ≥ 0)
(214) ((UIncreasing(908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[9]), x1[9], x3[9], x0[9], x2[9])), ≥)∧0 ≥ 0∧[(-1)bso_142] ≥ 0)
(215) ((UIncreasing(908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[9]), x1[9], x3[9], x0[9], x2[9])), ≥)∧0 ≥ 0∧[(-1)bso_142] ≥ 0)
(216) ((UIncreasing(908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[9]), x1[9], x3[9], x0[9], x2[9])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_142] ≥ 0)
(217) ((UIncreasing(908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[9]), x1[9], x3[9], x0[9], x2[9])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_142] ≥ 0)
(218) ((UIncreasing(908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[9]), x1[9], x3[9], x0[9], x2[9])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_142] ≥ 0)
(219) (233_0_length_ConstantStackPush(x1[8])=656_0_length_Return(x0[9])∧x2[8]=x2[9]∧x3[8]=x3[9]∧x1[8]=x1[9]∧233_0_length_ConstantStackPush(x2[9])=656_0_length_Return(x0[13])∧x1[9]=x1[13]∧x3[9]=x3[13]∧x0[9]=x0[13]∧x2[9]=java.lang.Object(List(x2[13])) ⇒ 867_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[9]), x2[9], x3[9], x1[9])≥NonInfC∧867_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[9]), x2[9], x3[9], x1[9])≥908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[9]), x1[9], x3[9], x0[9], x2[9])∧(UIncreasing(908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[9]), x1[9], x3[9], x0[9], x2[9])), ≥))
(220) (0=x91∧627_0_length_NULL(x91, x1[8])=656_0_length_Return(x0[9])∧1=x92∧627_0_length_NULL(x92, x2[13])=656_0_length_Return(x0[9]) ⇒ 867_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[9]), java.lang.Object(List(x2[13])), x3[8], x1[8])≥NonInfC∧867_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[9]), java.lang.Object(List(x2[13])), x3[8], x1[8])≥908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(java.lang.Object(List(x2[13]))), x1[8], x3[8], x0[9], java.lang.Object(List(x2[13])))∧(UIncreasing(908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[9]), x1[9], x3[9], x0[9], x2[9])), ≥))
(221) (656_0_length_Return(x93)=656_0_length_Return(x0[9])∧0=x93∧1=x92∧627_0_length_NULL(x92, x2[13])=656_0_length_Return(x0[9]) ⇒ 867_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[9]), java.lang.Object(List(x2[13])), x3[8], NULL)≥NonInfC∧867_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[9]), java.lang.Object(List(x2[13])), x3[8], NULL)≥908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(java.lang.Object(List(x2[13]))), NULL, x3[8], x0[9], java.lang.Object(List(x2[13])))∧(UIncreasing(908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[9]), x1[9], x3[9], x0[9], x2[9])), ≥))
(222) (Cond_627_0_length_NULL(>=(x95, 0), x95, java.lang.Object(List(x94)))=656_0_length_Return(x0[9])∧0=x95∧1=x92∧627_0_length_NULL(x92, x2[13])=656_0_length_Return(x0[9]) ⇒ 867_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[9]), java.lang.Object(List(x2[13])), x3[8], java.lang.Object(List(x94)))≥NonInfC∧867_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[9]), java.lang.Object(List(x2[13])), x3[8], java.lang.Object(List(x94)))≥908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(java.lang.Object(List(x2[13]))), java.lang.Object(List(x94)), x3[8], x0[9], java.lang.Object(List(x2[13])))∧(UIncreasing(908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[9]), x1[9], x3[9], x0[9], x2[9])), ≥))
(223) (1=x92∧627_0_length_NULL(x92, x2[13])=656_0_length_Return(0) ⇒ 867_1_MAIN_INVOKEMETHOD(656_0_length_Return(0), java.lang.Object(List(x2[13])), x3[8], NULL)≥NonInfC∧867_1_MAIN_INVOKEMETHOD(656_0_length_Return(0), java.lang.Object(List(x2[13])), x3[8], NULL)≥908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(java.lang.Object(List(x2[13]))), NULL, x3[8], 0, java.lang.Object(List(x2[13])))∧(UIncreasing(908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[9]), x1[9], x3[9], x0[9], x2[9])), ≥))
(224) (>=(x95, 0)=x101∧java.lang.Object(List(x94))=x102∧Cond_627_0_length_NULL(x101, x95, x102)=656_0_length_Return(x0[9])∧0=x95∧1=x92∧627_0_length_NULL(x92, x2[13])=656_0_length_Return(x0[9]) ⇒ 867_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[9]), java.lang.Object(List(x2[13])), x3[8], java.lang.Object(List(x94)))≥NonInfC∧867_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[9]), java.lang.Object(List(x2[13])), x3[8], java.lang.Object(List(x94)))≥908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(java.lang.Object(List(x2[13]))), java.lang.Object(List(x94)), x3[8], x0[9], java.lang.Object(List(x2[13])))∧(UIncreasing(908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[9]), x1[9], x3[9], x0[9], x2[9])), ≥))
(225) (656_0_length_Return(x96)=656_0_length_Return(0)∧1=x96 ⇒ 867_1_MAIN_INVOKEMETHOD(656_0_length_Return(0), java.lang.Object(List(NULL)), x3[8], NULL)≥NonInfC∧867_1_MAIN_INVOKEMETHOD(656_0_length_Return(0), java.lang.Object(List(NULL)), x3[8], NULL)≥908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(java.lang.Object(List(NULL))), NULL, x3[8], 0, java.lang.Object(List(NULL)))∧(UIncreasing(908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[9]), x1[9], x3[9], x0[9], x2[9])), ≥))
(226) (Cond_627_0_length_NULL(>=(x98, 0), x98, java.lang.Object(List(x97)))=656_0_length_Return(0)∧1=x98 ⇒ 867_1_MAIN_INVOKEMETHOD(656_0_length_Return(0), java.lang.Object(List(java.lang.Object(List(x97)))), x3[8], NULL)≥NonInfC∧867_1_MAIN_INVOKEMETHOD(656_0_length_Return(0), java.lang.Object(List(java.lang.Object(List(x97)))), x3[8], NULL)≥908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(java.lang.Object(List(java.lang.Object(List(x97))))), NULL, x3[8], 0, java.lang.Object(List(java.lang.Object(List(x97)))))∧(UIncreasing(908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[9]), x1[9], x3[9], x0[9], x2[9])), ≥))
(227) (Cond_627_0_length_NULL(TRUE, 1, java.lang.Object(List(x97)))=656_0_length_Return(0) ⇒ 867_1_MAIN_INVOKEMETHOD(656_0_length_Return(0), java.lang.Object(List(java.lang.Object(List(x97)))), x3[8], NULL)≥NonInfC∧867_1_MAIN_INVOKEMETHOD(656_0_length_Return(0), java.lang.Object(List(java.lang.Object(List(x97)))), x3[8], NULL)≥908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(java.lang.Object(List(java.lang.Object(List(x97))))), NULL, x3[8], 0, java.lang.Object(List(java.lang.Object(List(x97)))))∧(UIncreasing(908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[9]), x1[9], x3[9], x0[9], x2[9])), ≥))
(228) (656_0_length_Return(x103)=656_0_length_Return(x0[9])∧>=(x95, 0)=x101∧java.lang.Object(List(x94))=x102∧Cond_627_0_length_NULL(x101, x95, x102)=656_0_length_Return(x0[9])∧0=x95∧1=x103 ⇒ 867_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[9]), java.lang.Object(List(NULL)), x3[8], java.lang.Object(List(x94)))≥NonInfC∧867_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[9]), java.lang.Object(List(NULL)), x3[8], java.lang.Object(List(x94)))≥908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(java.lang.Object(List(NULL))), java.lang.Object(List(x94)), x3[8], x0[9], java.lang.Object(List(NULL)))∧(UIncreasing(908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[9]), x1[9], x3[9], x0[9], x2[9])), ≥))
(229) (Cond_627_0_length_NULL(>=(x105, 0), x105, java.lang.Object(List(x104)))=656_0_length_Return(x0[9])∧>=(x95, 0)=x101∧java.lang.Object(List(x94))=x102∧Cond_627_0_length_NULL(x101, x95, x102)=656_0_length_Return(x0[9])∧0=x95∧1=x105 ⇒ 867_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[9]), java.lang.Object(List(java.lang.Object(List(x104)))), x3[8], java.lang.Object(List(x94)))≥NonInfC∧867_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[9]), java.lang.Object(List(java.lang.Object(List(x104)))), x3[8], java.lang.Object(List(x94)))≥908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(java.lang.Object(List(java.lang.Object(List(x104))))), java.lang.Object(List(x94)), x3[8], x0[9], java.lang.Object(List(java.lang.Object(List(x104)))))∧(UIncreasing(908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[9]), x1[9], x3[9], x0[9], x2[9])), ≥))
(230) (Cond_627_0_length_NULL(TRUE, 0, java.lang.Object(List(x94)))=656_0_length_Return(1) ⇒ 867_1_MAIN_INVOKEMETHOD(656_0_length_Return(1), java.lang.Object(List(NULL)), x3[8], java.lang.Object(List(x94)))≥NonInfC∧867_1_MAIN_INVOKEMETHOD(656_0_length_Return(1), java.lang.Object(List(NULL)), x3[8], java.lang.Object(List(x94)))≥908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(java.lang.Object(List(NULL))), java.lang.Object(List(x94)), x3[8], 1, java.lang.Object(List(NULL)))∧(UIncreasing(908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[9]), x1[9], x3[9], x0[9], x2[9])), ≥))
(231) (Cond_627_0_length_NULL(TRUE, 0, java.lang.Object(List(x94)))=656_0_length_Return(x0[9])∧Cond_627_0_length_NULL(TRUE, 1, java.lang.Object(List(x104)))=656_0_length_Return(x0[9]) ⇒ 867_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[9]), java.lang.Object(List(java.lang.Object(List(x104)))), x3[8], java.lang.Object(List(x94)))≥NonInfC∧867_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[9]), java.lang.Object(List(java.lang.Object(List(x104)))), x3[8], java.lang.Object(List(x94)))≥908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(java.lang.Object(List(java.lang.Object(List(x104))))), java.lang.Object(List(x94)), x3[8], x0[9], java.lang.Object(List(java.lang.Object(List(x104)))))∧(UIncreasing(908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[9]), x1[9], x3[9], x0[9], x2[9])), ≥))
(232) ((UIncreasing(908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[9]), x1[9], x3[9], x0[9], x2[9])), ≥)∧0 ≥ 0∧[(-1)bso_142] ≥ 0)
(233) ((UIncreasing(908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[9]), x1[9], x3[9], x0[9], x2[9])), ≥)∧0 ≥ 0∧[(-1)bso_142] ≥ 0)
(234) ((UIncreasing(908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[9]), x1[9], x3[9], x0[9], x2[9])), ≥)∧0 ≥ 0∧[(-1)bso_142] ≥ 0)
(235) ((UIncreasing(908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[9]), x1[9], x3[9], x0[9], x2[9])), ≥)∧0 ≥ 0∧[(-1)bso_142] ≥ 0)
(236) ((UIncreasing(908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[9]), x1[9], x3[9], x0[9], x2[9])), ≥)∧0 ≥ 0∧[(-1)bso_142] ≥ 0)
(237) ((UIncreasing(908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[9]), x1[9], x3[9], x0[9], x2[9])), ≥)∧0 ≥ 0∧[(-1)bso_142] ≥ 0)
(238) ((UIncreasing(908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[9]), x1[9], x3[9], x0[9], x2[9])), ≥)∧0 ≥ 0∧[(-1)bso_142] ≥ 0)
(239) ((UIncreasing(908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[9]), x1[9], x3[9], x0[9], x2[9])), ≥)∧0 ≥ 0∧[(-1)bso_142] ≥ 0)
(240) ((UIncreasing(908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[9]), x1[9], x3[9], x0[9], x2[9])), ≥)∧0 ≥ 0∧[(-1)bso_142] ≥ 0)
(241) ((UIncreasing(908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[9]), x1[9], x3[9], x0[9], x2[9])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_142] ≥ 0)
(242) ((UIncreasing(908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[9]), x1[9], x3[9], x0[9], x2[9])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_142] ≥ 0)
(243) ((UIncreasing(908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[9]), x1[9], x3[9], x0[9], x2[9])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_142] ≥ 0)
(244) (!(=(x4[10], x0[10]))=TRUE∧656_0_length_Return(x0[10])=656_0_length_Return(x0[11])∧x1[10]=x1[11]∧java.lang.Object(List(x3[10]))=java.lang.Object(List(x3[11]))∧x4[10]=x4[11]∧x2[10]=x2[11] ⇒ 908_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[10]), x1[10], java.lang.Object(List(x3[10])), x4[10], x2[10])≥NonInfC∧908_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[10]), x1[10], java.lang.Object(List(x3[10])), x4[10], x2[10])≥COND_908_1_MAIN_INVOKEMETHOD(!(=(x4[10], x0[10])), 656_0_length_Return(x0[10]), x1[10], java.lang.Object(List(x3[10])), x4[10], x2[10])∧(UIncreasing(COND_908_1_MAIN_INVOKEMETHOD(!(=(x4[10], x0[10])), 656_0_length_Return(x0[10]), x1[10], java.lang.Object(List(x3[10])), x4[10], x2[10])), ≥))
(245) (!(=(x4[10], x0[10]))=TRUE ⇒ 908_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[10]), x1[10], java.lang.Object(List(x3[10])), x4[10], x2[10])≥NonInfC∧908_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[10]), x1[10], java.lang.Object(List(x3[10])), x4[10], x2[10])≥COND_908_1_MAIN_INVOKEMETHOD(!(=(x4[10], x0[10])), 656_0_length_Return(x0[10]), x1[10], java.lang.Object(List(x3[10])), x4[10], x2[10])∧(UIncreasing(COND_908_1_MAIN_INVOKEMETHOD(!(=(x4[10], x0[10])), 656_0_length_Return(x0[10]), x1[10], java.lang.Object(List(x3[10])), x4[10], x2[10])), ≥))
(246) (0 ≥ 0 ⇒ (UIncreasing(COND_908_1_MAIN_INVOKEMETHOD(!(=(x4[10], x0[10])), 656_0_length_Return(x0[10]), x1[10], java.lang.Object(List(x3[10])), x4[10], x2[10])), ≥)∧[(3)bni_143 + (-1)Bound*bni_143] + [bni_143]x2[10] + [(4)bni_143]x3[10] + [bni_143]x1[10] ≥ 0∧[(-1)bso_144] ≥ 0)
(247) (0 ≥ 0 ⇒ (UIncreasing(COND_908_1_MAIN_INVOKEMETHOD(!(=(x4[10], x0[10])), 656_0_length_Return(x0[10]), x1[10], java.lang.Object(List(x3[10])), x4[10], x2[10])), ≥)∧[(3)bni_143 + (-1)Bound*bni_143] + [bni_143]x2[10] + [(4)bni_143]x3[10] + [bni_143]x1[10] ≥ 0∧[(-1)bso_144] ≥ 0)
(248) (0 ≥ 0 ⇒ (UIncreasing(COND_908_1_MAIN_INVOKEMETHOD(!(=(x4[10], x0[10])), 656_0_length_Return(x0[10]), x1[10], java.lang.Object(List(x3[10])), x4[10], x2[10])), ≥)∧[(3)bni_143 + (-1)Bound*bni_143] + [bni_143]x2[10] + [(4)bni_143]x3[10] + [bni_143]x1[10] ≥ 0∧[(-1)bso_144] ≥ 0)
(249) (0 ≥ 0 ⇒ (UIncreasing(COND_908_1_MAIN_INVOKEMETHOD(!(=(x4[10], x0[10])), 656_0_length_Return(x0[10]), x1[10], java.lang.Object(List(x3[10])), x4[10], x2[10])), ≥)∧[bni_143] ≥ 0∧0 ≥ 0∧[(4)bni_143] ≥ 0∧[bni_143] ≥ 0∧0 ≥ 0∧[(3)bni_143 + (-1)Bound*bni_143] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_144] ≥ 0)
(250) (!(=(x4[10], x0[10]))=TRUE∧656_0_length_Return(x0[10])=656_0_length_Return(x0[11])∧x1[10]=x1[11]∧java.lang.Object(List(x3[10]))=java.lang.Object(List(x3[11]))∧x4[10]=x4[11]∧x2[10]=x2[11]∧1100_0_test_Load(x1[11], x2[11], x3[11])=2429_0_test_Return∧x1[11]=x0[12]∧x2[11]=x1[12]∧x3[11]=x2[12] ⇒ COND_908_1_MAIN_INVOKEMETHOD(TRUE, 656_0_length_Return(x0[11]), x1[11], java.lang.Object(List(x3[11])), x4[11], x2[11])≥NonInfC∧COND_908_1_MAIN_INVOKEMETHOD(TRUE, 656_0_length_Return(x0[11]), x1[11], java.lang.Object(List(x3[11])), x4[11], x2[11])≥1100_1_MAIN_INVOKEMETHOD(1100_0_test_Load(x1[11], x2[11], x3[11]), x1[11], x2[11], x3[11])∧(UIncreasing(1100_1_MAIN_INVOKEMETHOD(1100_0_test_Load(x1[11], x2[11], x3[11]), x1[11], x2[11], x3[11])), ≥))
(251) (!(=(x4[10], x0[10]))=TRUE∧1100_0_test_Load(x1[11], x2[11], x3[11])=2429_0_test_Return ⇒ COND_908_1_MAIN_INVOKEMETHOD(TRUE, 656_0_length_Return(x0[10]), x1[11], java.lang.Object(List(x3[11])), x4[10], x2[11])≥NonInfC∧COND_908_1_MAIN_INVOKEMETHOD(TRUE, 656_0_length_Return(x0[10]), x1[11], java.lang.Object(List(x3[11])), x4[10], x2[11])≥1100_1_MAIN_INVOKEMETHOD(1100_0_test_Load(x1[11], x2[11], x3[11]), x1[11], x2[11], x3[11])∧(UIncreasing(1100_1_MAIN_INVOKEMETHOD(1100_0_test_Load(x1[11], x2[11], x3[11]), x1[11], x2[11], x3[11])), ≥))
(252) (2390_0_test_NULL(x109, x108, x110)=2429_0_test_Return∧!(=(x4[10], x0[10]))=TRUE ⇒ COND_908_1_MAIN_INVOKEMETHOD(TRUE, 656_0_length_Return(x0[10]), x110, java.lang.Object(List(x108)), x4[10], x109)≥NonInfC∧COND_908_1_MAIN_INVOKEMETHOD(TRUE, 656_0_length_Return(x0[10]), x110, java.lang.Object(List(x108)), x4[10], x109)≥1100_1_MAIN_INVOKEMETHOD(1100_0_test_Load(x110, x109, x108), x110, x109, x108)∧(UIncreasing(1100_1_MAIN_INVOKEMETHOD(1100_0_test_Load(x1[11], x2[11], x3[11]), x1[11], x2[11], x3[11])), ≥))
(253) (0 ≥ 0 ⇒ (UIncreasing(1100_1_MAIN_INVOKEMETHOD(1100_0_test_Load(x1[11], x2[11], x3[11]), x1[11], x2[11], x3[11])), ≥)∧[(3)bni_145 + (-1)Bound*bni_145] + [bni_145]x109 + [(4)bni_145]x108 + [bni_145]x110 ≥ 0∧[1 + (-1)bso_146] + [3]x108 ≥ 0)
(254) (0 ≥ 0 ⇒ (UIncreasing(1100_1_MAIN_INVOKEMETHOD(1100_0_test_Load(x1[11], x2[11], x3[11]), x1[11], x2[11], x3[11])), ≥)∧[(3)bni_145 + (-1)Bound*bni_145] + [bni_145]x109 + [(4)bni_145]x108 + [bni_145]x110 ≥ 0∧[1 + (-1)bso_146] + [3]x108 ≥ 0)
(255) (0 ≥ 0 ⇒ (UIncreasing(1100_1_MAIN_INVOKEMETHOD(1100_0_test_Load(x1[11], x2[11], x3[11]), x1[11], x2[11], x3[11])), ≥)∧[(3)bni_145 + (-1)Bound*bni_145] + [bni_145]x109 + [(4)bni_145]x108 + [bni_145]x110 ≥ 0∧[1 + (-1)bso_146] + [3]x108 ≥ 0)
(256) (0 ≥ 0 ⇒ (UIncreasing(1100_1_MAIN_INVOKEMETHOD(1100_0_test_Load(x1[11], x2[11], x3[11]), x1[11], x2[11], x3[11])), ≥)∧[bni_145] ≥ 0∧0 ≥ 0∧[(4)bni_145] ≥ 0∧[bni_145] ≥ 0∧0 ≥ 0∧[(3)bni_145 + (-1)Bound*bni_145] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_146] ≥ 0∧[1] ≥ 0)
(257) (1100_0_test_Load(x1[11], x2[11], x3[11])=2429_0_test_Return∧x1[11]=x0[12]∧x2[11]=x1[12]∧x3[11]=x2[12]∧233_0_length_ConstantStackPush(x0[12])=656_0_length_Return(x0[0])∧x1[12]=x2[0]∧x2[12]=x3[0]∧x0[12]=x1[0] ⇒ 1100_1_MAIN_INVOKEMETHOD(2429_0_test_Return, x0[12], x1[12], x2[12])≥NonInfC∧1100_1_MAIN_INVOKEMETHOD(2429_0_test_Return, x0[12], x1[12], x2[12])≥233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x0[12]), x1[12], x2[12], x0[12])∧(UIncreasing(233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x0[12]), x1[12], x2[12], x0[12])), ≥))
(258) (1100_0_test_Load(x1[11], x2[11], x3[11])=2429_0_test_Return∧0=x111∧627_0_length_NULL(x111, x1[11])=656_0_length_Return(x0[0]) ⇒ 1100_1_MAIN_INVOKEMETHOD(2429_0_test_Return, x1[11], x2[11], x3[11])≥NonInfC∧1100_1_MAIN_INVOKEMETHOD(2429_0_test_Return, x1[11], x2[11], x3[11])≥233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x1[11]), x2[11], x3[11], x1[11])∧(UIncreasing(233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x0[12]), x1[12], x2[12], x0[12])), ≥))
(259) (2390_0_test_NULL(x113, x112, x114)=2429_0_test_Return∧0=x111∧627_0_length_NULL(x111, x114)=656_0_length_Return(x0[0]) ⇒ 1100_1_MAIN_INVOKEMETHOD(2429_0_test_Return, x114, x113, x112)≥NonInfC∧1100_1_MAIN_INVOKEMETHOD(2429_0_test_Return, x114, x113, x112)≥233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x114), x113, x112, x114)∧(UIncreasing(233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x0[12]), x1[12], x2[12], x0[12])), ≥))
(260) (656_0_length_Return(x115)=656_0_length_Return(x0[0])∧2390_0_test_NULL(x113, x112, NULL)=2429_0_test_Return∧0=x115 ⇒ 1100_1_MAIN_INVOKEMETHOD(2429_0_test_Return, NULL, x113, x112)≥NonInfC∧1100_1_MAIN_INVOKEMETHOD(2429_0_test_Return, NULL, x113, x112)≥233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(NULL), x113, x112, NULL)∧(UIncreasing(233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x0[12]), x1[12], x2[12], x0[12])), ≥))
(261) (Cond_627_0_length_NULL(>=(x117, 0), x117, java.lang.Object(List(x116)))=656_0_length_Return(x0[0])∧2390_0_test_NULL(x113, x112, java.lang.Object(List(x116)))=2429_0_test_Return∧0=x117 ⇒ 1100_1_MAIN_INVOKEMETHOD(2429_0_test_Return, java.lang.Object(List(x116)), x113, x112)≥NonInfC∧1100_1_MAIN_INVOKEMETHOD(2429_0_test_Return, java.lang.Object(List(x116)), x113, x112)≥233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(java.lang.Object(List(x116))), x113, x112, java.lang.Object(List(x116)))∧(UIncreasing(233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x0[12]), x1[12], x2[12], x0[12])), ≥))
(262) (1100_1_MAIN_INVOKEMETHOD(2429_0_test_Return, NULL, x113, x112)≥NonInfC∧1100_1_MAIN_INVOKEMETHOD(2429_0_test_Return, NULL, x113, x112)≥233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(NULL), x113, x112, NULL)∧(UIncreasing(233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x0[12]), x1[12], x2[12], x0[12])), ≥))
(263) (2390_0_test_NULL(x113, x112, java.lang.Object(List(x116)))=2429_0_test_Return∧Cond_627_0_length_NULL(TRUE, 0, java.lang.Object(List(x116)))=656_0_length_Return(x0[0]) ⇒ 1100_1_MAIN_INVOKEMETHOD(2429_0_test_Return, java.lang.Object(List(x116)), x113, x112)≥NonInfC∧1100_1_MAIN_INVOKEMETHOD(2429_0_test_Return, java.lang.Object(List(x116)), x113, x112)≥233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(java.lang.Object(List(x116))), x113, x112, java.lang.Object(List(x116)))∧(UIncreasing(233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x0[12]), x1[12], x2[12], x0[12])), ≥))
(264) ((UIncreasing(233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x0[12]), x1[12], x2[12], x0[12])), ≥)∧[3 + (-1)bso_148] ≥ 0)
(265) ((UIncreasing(233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x0[12]), x1[12], x2[12], x0[12])), ≥)∧0 ≥ 0∧[3 + (-1)bso_148] ≥ 0)
(266) ((UIncreasing(233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x0[12]), x1[12], x2[12], x0[12])), ≥)∧[3 + (-1)bso_148] ≥ 0)
(267) ((UIncreasing(233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x0[12]), x1[12], x2[12], x0[12])), ≥)∧0 ≥ 0∧[3 + (-1)bso_148] ≥ 0)
(268) ((UIncreasing(233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x0[12]), x1[12], x2[12], x0[12])), ≥)∧[3 + (-1)bso_148] ≥ 0)
(269) ((UIncreasing(233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x0[12]), x1[12], x2[12], x0[12])), ≥)∧0 ≥ 0∧[3 + (-1)bso_148] ≥ 0)
(270) ((UIncreasing(233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x0[12]), x1[12], x2[12], x0[12])), ≥)∧0 ≥ 0∧0 ≥ 0∧[3 + (-1)bso_148] ≥ 0)
(271) ((UIncreasing(233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x0[12]), x1[12], x2[12], x0[12])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[3 + (-1)bso_148] ≥ 0)
(272) (1100_0_test_Load(x1[13], x2[13], x3[13])=2429_0_test_Return∧x1[13]=x0[12]∧x2[13]=x1[12]∧x3[13]=x2[12]∧233_0_length_ConstantStackPush(x0[12])=656_0_length_Return(x0[0])∧x1[12]=x2[0]∧x2[12]=x3[0]∧x0[12]=x1[0] ⇒ 1100_1_MAIN_INVOKEMETHOD(2429_0_test_Return, x0[12], x1[12], x2[12])≥NonInfC∧1100_1_MAIN_INVOKEMETHOD(2429_0_test_Return, x0[12], x1[12], x2[12])≥233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x0[12]), x1[12], x2[12], x0[12])∧(UIncreasing(233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x0[12]), x1[12], x2[12], x0[12])), ≥))
(273) (1100_0_test_Load(x1[13], x2[13], x3[13])=2429_0_test_Return∧0=x120∧627_0_length_NULL(x120, x1[13])=656_0_length_Return(x0[0]) ⇒ 1100_1_MAIN_INVOKEMETHOD(2429_0_test_Return, x1[13], x2[13], x3[13])≥NonInfC∧1100_1_MAIN_INVOKEMETHOD(2429_0_test_Return, x1[13], x2[13], x3[13])≥233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x1[13]), x2[13], x3[13], x1[13])∧(UIncreasing(233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x0[12]), x1[12], x2[12], x0[12])), ≥))
(274) (2390_0_test_NULL(x122, x121, x123)=2429_0_test_Return∧0=x120∧627_0_length_NULL(x120, x123)=656_0_length_Return(x0[0]) ⇒ 1100_1_MAIN_INVOKEMETHOD(2429_0_test_Return, x123, x122, x121)≥NonInfC∧1100_1_MAIN_INVOKEMETHOD(2429_0_test_Return, x123, x122, x121)≥233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x123), x122, x121, x123)∧(UIncreasing(233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x0[12]), x1[12], x2[12], x0[12])), ≥))
(275) (656_0_length_Return(x124)=656_0_length_Return(x0[0])∧2390_0_test_NULL(x122, x121, NULL)=2429_0_test_Return∧0=x124 ⇒ 1100_1_MAIN_INVOKEMETHOD(2429_0_test_Return, NULL, x122, x121)≥NonInfC∧1100_1_MAIN_INVOKEMETHOD(2429_0_test_Return, NULL, x122, x121)≥233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(NULL), x122, x121, NULL)∧(UIncreasing(233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x0[12]), x1[12], x2[12], x0[12])), ≥))
(276) (Cond_627_0_length_NULL(>=(x126, 0), x126, java.lang.Object(List(x125)))=656_0_length_Return(x0[0])∧2390_0_test_NULL(x122, x121, java.lang.Object(List(x125)))=2429_0_test_Return∧0=x126 ⇒ 1100_1_MAIN_INVOKEMETHOD(2429_0_test_Return, java.lang.Object(List(x125)), x122, x121)≥NonInfC∧1100_1_MAIN_INVOKEMETHOD(2429_0_test_Return, java.lang.Object(List(x125)), x122, x121)≥233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(java.lang.Object(List(x125))), x122, x121, java.lang.Object(List(x125)))∧(UIncreasing(233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x0[12]), x1[12], x2[12], x0[12])), ≥))
(277) (1100_1_MAIN_INVOKEMETHOD(2429_0_test_Return, NULL, x122, x121)≥NonInfC∧1100_1_MAIN_INVOKEMETHOD(2429_0_test_Return, NULL, x122, x121)≥233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(NULL), x122, x121, NULL)∧(UIncreasing(233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x0[12]), x1[12], x2[12], x0[12])), ≥))
(278) (2390_0_test_NULL(x122, x121, java.lang.Object(List(x125)))=2429_0_test_Return∧Cond_627_0_length_NULL(TRUE, 0, java.lang.Object(List(x125)))=656_0_length_Return(x0[0]) ⇒ 1100_1_MAIN_INVOKEMETHOD(2429_0_test_Return, java.lang.Object(List(x125)), x122, x121)≥NonInfC∧1100_1_MAIN_INVOKEMETHOD(2429_0_test_Return, java.lang.Object(List(x125)), x122, x121)≥233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(java.lang.Object(List(x125))), x122, x121, java.lang.Object(List(x125)))∧(UIncreasing(233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x0[12]), x1[12], x2[12], x0[12])), ≥))
(279) ((UIncreasing(233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x0[12]), x1[12], x2[12], x0[12])), ≥)∧[3 + (-1)bso_148] ≥ 0)
(280) ((UIncreasing(233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x0[12]), x1[12], x2[12], x0[12])), ≥)∧0 ≥ 0∧[3 + (-1)bso_148] ≥ 0)
(281) ((UIncreasing(233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x0[12]), x1[12], x2[12], x0[12])), ≥)∧[3 + (-1)bso_148] ≥ 0)
(282) ((UIncreasing(233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x0[12]), x1[12], x2[12], x0[12])), ≥)∧0 ≥ 0∧[3 + (-1)bso_148] ≥ 0)
(283) ((UIncreasing(233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x0[12]), x1[12], x2[12], x0[12])), ≥)∧[3 + (-1)bso_148] ≥ 0)
(284) ((UIncreasing(233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x0[12]), x1[12], x2[12], x0[12])), ≥)∧0 ≥ 0∧[3 + (-1)bso_148] ≥ 0)
(285) ((UIncreasing(233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x0[12]), x1[12], x2[12], x0[12])), ≥)∧0 ≥ 0∧0 ≥ 0∧[3 + (-1)bso_148] ≥ 0)
(286) ((UIncreasing(233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x0[12]), x1[12], x2[12], x0[12])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[3 + (-1)bso_148] ≥ 0)
(287) (1100_0_test_Load(x1[15], x2[15], x3[15])=2429_0_test_Return∧x1[15]=x0[12]∧x2[15]=x1[12]∧x3[15]=x2[12]∧233_0_length_ConstantStackPush(x0[12])=656_0_length_Return(x0[0])∧x1[12]=x2[0]∧x2[12]=x3[0]∧x0[12]=x1[0] ⇒ 1100_1_MAIN_INVOKEMETHOD(2429_0_test_Return, x0[12], x1[12], x2[12])≥NonInfC∧1100_1_MAIN_INVOKEMETHOD(2429_0_test_Return, x0[12], x1[12], x2[12])≥233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x0[12]), x1[12], x2[12], x0[12])∧(UIncreasing(233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x0[12]), x1[12], x2[12], x0[12])), ≥))
(288) (1100_0_test_Load(x1[15], x2[15], x3[15])=2429_0_test_Return∧0=x129∧627_0_length_NULL(x129, x1[15])=656_0_length_Return(x0[0]) ⇒ 1100_1_MAIN_INVOKEMETHOD(2429_0_test_Return, x1[15], x2[15], x3[15])≥NonInfC∧1100_1_MAIN_INVOKEMETHOD(2429_0_test_Return, x1[15], x2[15], x3[15])≥233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x1[15]), x2[15], x3[15], x1[15])∧(UIncreasing(233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x0[12]), x1[12], x2[12], x0[12])), ≥))
(289) (2390_0_test_NULL(x131, x130, x132)=2429_0_test_Return∧0=x129∧627_0_length_NULL(x129, x132)=656_0_length_Return(x0[0]) ⇒ 1100_1_MAIN_INVOKEMETHOD(2429_0_test_Return, x132, x131, x130)≥NonInfC∧1100_1_MAIN_INVOKEMETHOD(2429_0_test_Return, x132, x131, x130)≥233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x132), x131, x130, x132)∧(UIncreasing(233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x0[12]), x1[12], x2[12], x0[12])), ≥))
(290) (656_0_length_Return(x133)=656_0_length_Return(x0[0])∧2390_0_test_NULL(x131, x130, NULL)=2429_0_test_Return∧0=x133 ⇒ 1100_1_MAIN_INVOKEMETHOD(2429_0_test_Return, NULL, x131, x130)≥NonInfC∧1100_1_MAIN_INVOKEMETHOD(2429_0_test_Return, NULL, x131, x130)≥233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(NULL), x131, x130, NULL)∧(UIncreasing(233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x0[12]), x1[12], x2[12], x0[12])), ≥))
(291) (Cond_627_0_length_NULL(>=(x135, 0), x135, java.lang.Object(List(x134)))=656_0_length_Return(x0[0])∧2390_0_test_NULL(x131, x130, java.lang.Object(List(x134)))=2429_0_test_Return∧0=x135 ⇒ 1100_1_MAIN_INVOKEMETHOD(2429_0_test_Return, java.lang.Object(List(x134)), x131, x130)≥NonInfC∧1100_1_MAIN_INVOKEMETHOD(2429_0_test_Return, java.lang.Object(List(x134)), x131, x130)≥233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(java.lang.Object(List(x134))), x131, x130, java.lang.Object(List(x134)))∧(UIncreasing(233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x0[12]), x1[12], x2[12], x0[12])), ≥))
(292) (1100_1_MAIN_INVOKEMETHOD(2429_0_test_Return, NULL, x131, x130)≥NonInfC∧1100_1_MAIN_INVOKEMETHOD(2429_0_test_Return, NULL, x131, x130)≥233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(NULL), x131, x130, NULL)∧(UIncreasing(233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x0[12]), x1[12], x2[12], x0[12])), ≥))
(293) (2390_0_test_NULL(x131, x130, java.lang.Object(List(x134)))=2429_0_test_Return∧Cond_627_0_length_NULL(TRUE, 0, java.lang.Object(List(x134)))=656_0_length_Return(x0[0]) ⇒ 1100_1_MAIN_INVOKEMETHOD(2429_0_test_Return, java.lang.Object(List(x134)), x131, x130)≥NonInfC∧1100_1_MAIN_INVOKEMETHOD(2429_0_test_Return, java.lang.Object(List(x134)), x131, x130)≥233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(java.lang.Object(List(x134))), x131, x130, java.lang.Object(List(x134)))∧(UIncreasing(233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x0[12]), x1[12], x2[12], x0[12])), ≥))
(294) ((UIncreasing(233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x0[12]), x1[12], x2[12], x0[12])), ≥)∧[3 + (-1)bso_148] ≥ 0)
(295) ((UIncreasing(233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x0[12]), x1[12], x2[12], x0[12])), ≥)∧0 ≥ 0∧[3 + (-1)bso_148] ≥ 0)
(296) ((UIncreasing(233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x0[12]), x1[12], x2[12], x0[12])), ≥)∧[3 + (-1)bso_148] ≥ 0)
(297) ((UIncreasing(233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x0[12]), x1[12], x2[12], x0[12])), ≥)∧0 ≥ 0∧[3 + (-1)bso_148] ≥ 0)
(298) ((UIncreasing(233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x0[12]), x1[12], x2[12], x0[12])), ≥)∧[3 + (-1)bso_148] ≥ 0)
(299) ((UIncreasing(233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x0[12]), x1[12], x2[12], x0[12])), ≥)∧0 ≥ 0∧[3 + (-1)bso_148] ≥ 0)
(300) ((UIncreasing(233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x0[12]), x1[12], x2[12], x0[12])), ≥)∧0 ≥ 0∧0 ≥ 0∧[3 + (-1)bso_148] ≥ 0)
(301) ((UIncreasing(233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x0[12]), x1[12], x2[12], x0[12])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[3 + (-1)bso_148] ≥ 0)
(302) (233_0_length_ConstantStackPush(x2[9])=656_0_length_Return(x0[13])∧x1[9]=x1[13]∧x3[9]=x3[13]∧x0[9]=x0[13]∧x2[9]=java.lang.Object(List(x2[13]))∧1100_0_test_Load(x1[13], x2[13], x3[13])=2429_0_test_Return∧x1[13]=x0[12]∧x2[13]=x1[12]∧x3[13]=x2[12] ⇒ 908_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[13]), x1[13], x3[13], x0[13], java.lang.Object(List(x2[13])))≥NonInfC∧908_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[13]), x1[13], x3[13], x0[13], java.lang.Object(List(x2[13])))≥1100_1_MAIN_INVOKEMETHOD(1100_0_test_Load(x1[13], x2[13], x3[13]), x1[13], x2[13], x3[13])∧(UIncreasing(1100_1_MAIN_INVOKEMETHOD(1100_0_test_Load(x1[13], x2[13], x3[13]), x1[13], x2[13], x3[13])), ≥))
(303) (1100_0_test_Load(x1[13], x2[13], x3[13])=2429_0_test_Return∧1=x138∧627_0_length_NULL(x138, x2[13])=656_0_length_Return(x0[9]) ⇒ 908_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[9]), x1[13], x3[13], x0[9], java.lang.Object(List(x2[13])))≥NonInfC∧908_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[9]), x1[13], x3[13], x0[9], java.lang.Object(List(x2[13])))≥1100_1_MAIN_INVOKEMETHOD(1100_0_test_Load(x1[13], x2[13], x3[13]), x1[13], x2[13], x3[13])∧(UIncreasing(1100_1_MAIN_INVOKEMETHOD(1100_0_test_Load(x1[13], x2[13], x3[13]), x1[13], x2[13], x3[13])), ≥))
(304) (2390_0_test_NULL(x140, x139, x141)=2429_0_test_Return∧1=x138∧627_0_length_NULL(x138, x140)=656_0_length_Return(x0[9]) ⇒ 908_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[9]), x141, x139, x0[9], java.lang.Object(List(x140)))≥NonInfC∧908_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[9]), x141, x139, x0[9], java.lang.Object(List(x140)))≥1100_1_MAIN_INVOKEMETHOD(1100_0_test_Load(x141, x140, x139), x141, x140, x139)∧(UIncreasing(1100_1_MAIN_INVOKEMETHOD(1100_0_test_Load(x1[13], x2[13], x3[13]), x1[13], x2[13], x3[13])), ≥))
(305) (656_0_length_Return(x142)=656_0_length_Return(x0[9])∧2390_0_test_NULL(NULL, x139, x141)=2429_0_test_Return∧1=x142 ⇒ 908_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[9]), x141, x139, x0[9], java.lang.Object(List(NULL)))≥NonInfC∧908_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[9]), x141, x139, x0[9], java.lang.Object(List(NULL)))≥1100_1_MAIN_INVOKEMETHOD(1100_0_test_Load(x141, NULL, x139), x141, NULL, x139)∧(UIncreasing(1100_1_MAIN_INVOKEMETHOD(1100_0_test_Load(x1[13], x2[13], x3[13]), x1[13], x2[13], x3[13])), ≥))
(306) (Cond_627_0_length_NULL(>=(x144, 0), x144, java.lang.Object(List(x143)))=656_0_length_Return(x0[9])∧2390_0_test_NULL(java.lang.Object(List(x143)), x139, x141)=2429_0_test_Return∧1=x144 ⇒ 908_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[9]), x141, x139, x0[9], java.lang.Object(List(java.lang.Object(List(x143)))))≥NonInfC∧908_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[9]), x141, x139, x0[9], java.lang.Object(List(java.lang.Object(List(x143)))))≥1100_1_MAIN_INVOKEMETHOD(1100_0_test_Load(x141, java.lang.Object(List(x143)), x139), x141, java.lang.Object(List(x143)), x139)∧(UIncreasing(1100_1_MAIN_INVOKEMETHOD(1100_0_test_Load(x1[13], x2[13], x3[13]), x1[13], x2[13], x3[13])), ≥))
(307) (2390_0_test_NULL(NULL, x139, x141)=2429_0_test_Return ⇒ 908_1_MAIN_INVOKEMETHOD(656_0_length_Return(1), x141, x139, 1, java.lang.Object(List(NULL)))≥NonInfC∧908_1_MAIN_INVOKEMETHOD(656_0_length_Return(1), x141, x139, 1, java.lang.Object(List(NULL)))≥1100_1_MAIN_INVOKEMETHOD(1100_0_test_Load(x141, NULL, x139), x141, NULL, x139)∧(UIncreasing(1100_1_MAIN_INVOKEMETHOD(1100_0_test_Load(x1[13], x2[13], x3[13]), x1[13], x2[13], x3[13])), ≥))
(308) (2390_0_test_NULL(java.lang.Object(List(x143)), x139, x141)=2429_0_test_Return∧Cond_627_0_length_NULL(TRUE, 1, java.lang.Object(List(x143)))=656_0_length_Return(x0[9]) ⇒ 908_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[9]), x141, x139, x0[9], java.lang.Object(List(java.lang.Object(List(x143)))))≥NonInfC∧908_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[9]), x141, x139, x0[9], java.lang.Object(List(java.lang.Object(List(x143)))))≥1100_1_MAIN_INVOKEMETHOD(1100_0_test_Load(x141, java.lang.Object(List(x143)), x139), x141, java.lang.Object(List(x143)), x139)∧(UIncreasing(1100_1_MAIN_INVOKEMETHOD(1100_0_test_Load(x1[13], x2[13], x3[13]), x1[13], x2[13], x3[13])), ≥))
(309) ((UIncreasing(1100_1_MAIN_INVOKEMETHOD(1100_0_test_Load(x1[13], x2[13], x3[13]), x1[13], x2[13], x3[13])), ≥)∧[(3)bni_149 + (-1)Bound*bni_149] + [bni_149]x139 + [bni_149]x141 ≥ 0∧[1 + (-1)bso_150] ≥ 0)
(310) ((UIncreasing(1100_1_MAIN_INVOKEMETHOD(1100_0_test_Load(x1[13], x2[13], x3[13]), x1[13], x2[13], x3[13])), ≥)∧[(19)bni_149 + (-1)Bound*bni_149] + [(16)bni_149]x143 + [bni_149]x139 + [bni_149]x141 ≥ 0∧[13 + (-1)bso_150] + [12]x143 ≥ 0)
(311) ((UIncreasing(1100_1_MAIN_INVOKEMETHOD(1100_0_test_Load(x1[13], x2[13], x3[13]), x1[13], x2[13], x3[13])), ≥)∧[(3)bni_149 + (-1)Bound*bni_149] + [bni_149]x139 + [bni_149]x141 ≥ 0∧[1 + (-1)bso_150] ≥ 0)
(312) ((UIncreasing(1100_1_MAIN_INVOKEMETHOD(1100_0_test_Load(x1[13], x2[13], x3[13]), x1[13], x2[13], x3[13])), ≥)∧[(19)bni_149 + (-1)Bound*bni_149] + [(16)bni_149]x143 + [bni_149]x139 + [bni_149]x141 ≥ 0∧[13 + (-1)bso_150] + [12]x143 ≥ 0)
(313) ((UIncreasing(1100_1_MAIN_INVOKEMETHOD(1100_0_test_Load(x1[13], x2[13], x3[13]), x1[13], x2[13], x3[13])), ≥)∧[(3)bni_149 + (-1)Bound*bni_149] + [bni_149]x139 + [bni_149]x141 ≥ 0∧[1 + (-1)bso_150] ≥ 0)
(314) ((UIncreasing(1100_1_MAIN_INVOKEMETHOD(1100_0_test_Load(x1[13], x2[13], x3[13]), x1[13], x2[13], x3[13])), ≥)∧[(19)bni_149 + (-1)Bound*bni_149] + [(16)bni_149]x143 + [bni_149]x139 + [bni_149]x141 ≥ 0∧[13 + (-1)bso_150] + [12]x143 ≥ 0)
(315) ((UIncreasing(1100_1_MAIN_INVOKEMETHOD(1100_0_test_Load(x1[13], x2[13], x3[13]), x1[13], x2[13], x3[13])), ≥)∧[bni_149] ≥ 0∧[bni_149] ≥ 0∧[(3)bni_149 + (-1)Bound*bni_149] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_150] ≥ 0)
(316) ((UIncreasing(1100_1_MAIN_INVOKEMETHOD(1100_0_test_Load(x1[13], x2[13], x3[13]), x1[13], x2[13], x3[13])), ≥)∧[(16)bni_149] ≥ 0∧0 ≥ 0∧[bni_149] ≥ 0∧[bni_149] ≥ 0∧[(19)bni_149 + (-1)Bound*bni_149] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[13 + (-1)bso_150] ≥ 0∧[1] ≥ 0)
(317) (>(x4[14], x0[14])=TRUE∧656_0_length_Return(x0[14])=656_0_length_Return(x0[15])∧java.lang.Object(List(x1[14]))=java.lang.Object(List(x1[15]))∧x3[14]=x3[15]∧x4[14]=x4[15]∧x2[14]=x2[15] ⇒ 807_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[14]), java.lang.Object(List(x1[14])), x3[14], x4[14], x2[14])≥NonInfC∧807_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[14]), java.lang.Object(List(x1[14])), x3[14], x4[14], x2[14])≥COND_807_1_MAIN_INVOKEMETHOD1(>(x4[14], x0[14]), 656_0_length_Return(x0[14]), java.lang.Object(List(x1[14])), x3[14], x4[14], x2[14])∧(UIncreasing(COND_807_1_MAIN_INVOKEMETHOD1(>(x4[14], x0[14]), 656_0_length_Return(x0[14]), java.lang.Object(List(x1[14])), x3[14], x4[14], x2[14])), ≥))
(318) (>(x4[14], x0[14])=TRUE ⇒ 807_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[14]), java.lang.Object(List(x1[14])), x3[14], x4[14], x2[14])≥NonInfC∧807_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[14]), java.lang.Object(List(x1[14])), x3[14], x4[14], x2[14])≥COND_807_1_MAIN_INVOKEMETHOD1(>(x4[14], x0[14]), 656_0_length_Return(x0[14]), java.lang.Object(List(x1[14])), x3[14], x4[14], x2[14])∧(UIncreasing(COND_807_1_MAIN_INVOKEMETHOD1(>(x4[14], x0[14]), 656_0_length_Return(x0[14]), java.lang.Object(List(x1[14])), x3[14], x4[14], x2[14])), ≥))
(319) (0 ≥ 0 ⇒ (UIncreasing(COND_807_1_MAIN_INVOKEMETHOD1(>(x4[14], x0[14]), 656_0_length_Return(x0[14]), java.lang.Object(List(x1[14])), x3[14], x4[14], x2[14])), ≥)∧[(3)bni_151 + (-1)Bound*bni_151] + [bni_151]x2[14] + [bni_151]x3[14] + [(4)bni_151]x1[14] ≥ 0∧[(-1)bso_152] ≥ 0)
(320) (0 ≥ 0 ⇒ (UIncreasing(COND_807_1_MAIN_INVOKEMETHOD1(>(x4[14], x0[14]), 656_0_length_Return(x0[14]), java.lang.Object(List(x1[14])), x3[14], x4[14], x2[14])), ≥)∧[(3)bni_151 + (-1)Bound*bni_151] + [bni_151]x2[14] + [bni_151]x3[14] + [(4)bni_151]x1[14] ≥ 0∧[(-1)bso_152] ≥ 0)
(321) (0 ≥ 0 ⇒ (UIncreasing(COND_807_1_MAIN_INVOKEMETHOD1(>(x4[14], x0[14]), 656_0_length_Return(x0[14]), java.lang.Object(List(x1[14])), x3[14], x4[14], x2[14])), ≥)∧[(3)bni_151 + (-1)Bound*bni_151] + [bni_151]x2[14] + [bni_151]x3[14] + [(4)bni_151]x1[14] ≥ 0∧[(-1)bso_152] ≥ 0)
(322) (0 ≥ 0 ⇒ (UIncreasing(COND_807_1_MAIN_INVOKEMETHOD1(>(x4[14], x0[14]), 656_0_length_Return(x0[14]), java.lang.Object(List(x1[14])), x3[14], x4[14], x2[14])), ≥)∧[bni_151] ≥ 0∧0 ≥ 0∧[bni_151] ≥ 0∧[(4)bni_151] ≥ 0∧0 ≥ 0∧[(3)bni_151 + (-1)Bound*bni_151] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_152] ≥ 0)
(323) (>(x4[14], x0[14])=TRUE∧656_0_length_Return(x0[14])=656_0_length_Return(x0[15])∧java.lang.Object(List(x1[14]))=java.lang.Object(List(x1[15]))∧x3[14]=x3[15]∧x4[14]=x4[15]∧x2[14]=x2[15]∧1100_0_test_Load(x1[15], x2[15], x3[15])=2429_0_test_Return∧x1[15]=x0[12]∧x2[15]=x1[12]∧x3[15]=x2[12] ⇒ COND_807_1_MAIN_INVOKEMETHOD1(TRUE, 656_0_length_Return(x0[15]), java.lang.Object(List(x1[15])), x3[15], x4[15], x2[15])≥NonInfC∧COND_807_1_MAIN_INVOKEMETHOD1(TRUE, 656_0_length_Return(x0[15]), java.lang.Object(List(x1[15])), x3[15], x4[15], x2[15])≥1100_1_MAIN_INVOKEMETHOD(1100_0_test_Load(x1[15], x2[15], x3[15]), x1[15], x2[15], x3[15])∧(UIncreasing(1100_1_MAIN_INVOKEMETHOD(1100_0_test_Load(x1[15], x2[15], x3[15]), x1[15], x2[15], x3[15])), ≥))
(324) (>(x4[14], x0[14])=TRUE∧1100_0_test_Load(x1[15], x2[15], x3[15])=2429_0_test_Return ⇒ COND_807_1_MAIN_INVOKEMETHOD1(TRUE, 656_0_length_Return(x0[14]), java.lang.Object(List(x1[15])), x3[15], x4[14], x2[15])≥NonInfC∧COND_807_1_MAIN_INVOKEMETHOD1(TRUE, 656_0_length_Return(x0[14]), java.lang.Object(List(x1[15])), x3[15], x4[14], x2[15])≥1100_1_MAIN_INVOKEMETHOD(1100_0_test_Load(x1[15], x2[15], x3[15]), x1[15], x2[15], x3[15])∧(UIncreasing(1100_1_MAIN_INVOKEMETHOD(1100_0_test_Load(x1[15], x2[15], x3[15]), x1[15], x2[15], x3[15])), ≥))
(325) (2390_0_test_NULL(x149, x148, x150)=2429_0_test_Return∧>(x4[14], x0[14])=TRUE ⇒ COND_807_1_MAIN_INVOKEMETHOD1(TRUE, 656_0_length_Return(x0[14]), java.lang.Object(List(x150)), x148, x4[14], x149)≥NonInfC∧COND_807_1_MAIN_INVOKEMETHOD1(TRUE, 656_0_length_Return(x0[14]), java.lang.Object(List(x150)), x148, x4[14], x149)≥1100_1_MAIN_INVOKEMETHOD(1100_0_test_Load(x150, x149, x148), x150, x149, x148)∧(UIncreasing(1100_1_MAIN_INVOKEMETHOD(1100_0_test_Load(x1[15], x2[15], x3[15]), x1[15], x2[15], x3[15])), ≥))
(326) (0 ≥ 0 ⇒ (UIncreasing(1100_1_MAIN_INVOKEMETHOD(1100_0_test_Load(x1[15], x2[15], x3[15]), x1[15], x2[15], x3[15])), ≥)∧[(3)bni_153 + (-1)Bound*bni_153] + [bni_153]x149 + [bni_153]x148 + [(4)bni_153]x150 ≥ 0∧[1 + (-1)bso_154] + [3]x150 ≥ 0)
(327) (0 ≥ 0 ⇒ (UIncreasing(1100_1_MAIN_INVOKEMETHOD(1100_0_test_Load(x1[15], x2[15], x3[15]), x1[15], x2[15], x3[15])), ≥)∧[(3)bni_153 + (-1)Bound*bni_153] + [bni_153]x149 + [bni_153]x148 + [(4)bni_153]x150 ≥ 0∧[1 + (-1)bso_154] + [3]x150 ≥ 0)
(328) (0 ≥ 0 ⇒ (UIncreasing(1100_1_MAIN_INVOKEMETHOD(1100_0_test_Load(x1[15], x2[15], x3[15]), x1[15], x2[15], x3[15])), ≥)∧[(3)bni_153 + (-1)Bound*bni_153] + [bni_153]x149 + [bni_153]x148 + [(4)bni_153]x150 ≥ 0∧[1 + (-1)bso_154] + [3]x150 ≥ 0)
(329) (0 ≥ 0 ⇒ (UIncreasing(1100_1_MAIN_INVOKEMETHOD(1100_0_test_Load(x1[15], x2[15], x3[15]), x1[15], x2[15], x3[15])), ≥)∧[bni_153] ≥ 0∧0 ≥ 0∧[bni_153] ≥ 0∧[(4)bni_153] ≥ 0∧0 ≥ 0∧[(3)bni_153 + (-1)Bound*bni_153] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_154] ≥ 0∧[1] ≥ 0)
(330) (=(0, %(x0[16], 5))=TRUE∧656_0_length_Return(x0[16])=656_0_length_Return(x0[17])∧x1[16]=x1[17]∧x2[16]=x2[17]∧java.lang.Object(List(x3[16]))=java.lang.Object(List(x3[17])) ⇒ 718_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[16]), x1[16], x2[16], java.lang.Object(List(x3[16])))≥NonInfC∧718_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[16]), x1[16], x2[16], java.lang.Object(List(x3[16])))≥COND_718_1_MAIN_INVOKEMETHOD1(=(0, %(x0[16], 5)), 656_0_length_Return(x0[16]), x1[16], x2[16], java.lang.Object(List(x3[16])))∧(UIncreasing(COND_718_1_MAIN_INVOKEMETHOD1(=(0, %(x0[16], 5)), 656_0_length_Return(x0[16]), x1[16], x2[16], java.lang.Object(List(x3[16])))), ≥))
(331) (=(0, %(x0[16], 5))=TRUE ⇒ 718_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[16]), x1[16], x2[16], java.lang.Object(List(x3[16])))≥NonInfC∧718_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[16]), x1[16], x2[16], java.lang.Object(List(x3[16])))≥COND_718_1_MAIN_INVOKEMETHOD1(=(0, %(x0[16], 5)), 656_0_length_Return(x0[16]), x1[16], x2[16], java.lang.Object(List(x3[16])))∧(UIncreasing(COND_718_1_MAIN_INVOKEMETHOD1(=(0, %(x0[16], 5)), 656_0_length_Return(x0[16]), x1[16], x2[16], java.lang.Object(List(x3[16])))), ≥))
(332) (0 ≥ 0 ⇒ (UIncreasing(COND_718_1_MAIN_INVOKEMETHOD1(=(0, %(x0[16], 5)), 656_0_length_Return(x0[16]), x1[16], x2[16], java.lang.Object(List(x3[16])))), ≥)∧[(3)bni_155 + (-1)Bound*bni_155] + [(4)bni_155]x3[16] + [bni_155]x2[16] + [bni_155]x1[16] ≥ 0∧[(-1)bso_156] ≥ 0)
(333) (0 ≥ 0 ⇒ (UIncreasing(COND_718_1_MAIN_INVOKEMETHOD1(=(0, %(x0[16], 5)), 656_0_length_Return(x0[16]), x1[16], x2[16], java.lang.Object(List(x3[16])))), ≥)∧[(3)bni_155 + (-1)Bound*bni_155] + [(4)bni_155]x3[16] + [bni_155]x2[16] + [bni_155]x1[16] ≥ 0∧[(-1)bso_156] ≥ 0)
(334) (0 ≥ 0 ⇒ (UIncreasing(COND_718_1_MAIN_INVOKEMETHOD1(=(0, %(x0[16], 5)), 656_0_length_Return(x0[16]), x1[16], x2[16], java.lang.Object(List(x3[16])))), ≥)∧[(3)bni_155 + (-1)Bound*bni_155] + [(4)bni_155]x3[16] + [bni_155]x2[16] + [bni_155]x1[16] ≥ 0∧[(-1)bso_156] ≥ 0)
(335) (0 ≥ 0 ⇒ (UIncreasing(COND_718_1_MAIN_INVOKEMETHOD1(=(0, %(x0[16], 5)), 656_0_length_Return(x0[16]), x1[16], x2[16], java.lang.Object(List(x3[16])))), ≥)∧[(4)bni_155] ≥ 0∧[bni_155] ≥ 0∧[bni_155] ≥ 0∧0 ≥ 0∧[(3)bni_155 + (-1)Bound*bni_155] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_156] ≥ 0)
(336) (=(0, %(x0[16], 5))=TRUE∧656_0_length_Return(x0[16])=656_0_length_Return(x0[17])∧x1[16]=x1[17]∧x2[16]=x2[17]∧java.lang.Object(List(x3[16]))=java.lang.Object(List(x3[17]))∧233_0_length_ConstantStackPush(x1[17])=656_0_length_Return(x0[6])∧x2[17]=x2[6]∧x3[17]=x3[6]∧x1[17]=x1[6] ⇒ COND_718_1_MAIN_INVOKEMETHOD1(TRUE, 656_0_length_Return(x0[17]), x1[17], x2[17], java.lang.Object(List(x3[17])))≥NonInfC∧COND_718_1_MAIN_INVOKEMETHOD1(TRUE, 656_0_length_Return(x0[17]), x1[17], x2[17], java.lang.Object(List(x3[17])))≥775_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x1[17]), x2[17], x3[17], x1[17])∧(UIncreasing(775_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x1[17]), x2[17], x3[17], x1[17])), ≥))
(337) (=(0, %(x0[16], 5))=TRUE∧627_0_length_NULL(0, x1[17])=656_0_length_Return(x0[6]) ⇒ COND_718_1_MAIN_INVOKEMETHOD1(TRUE, 656_0_length_Return(x0[16]), x1[17], x2[16], java.lang.Object(List(x3[16])))≥NonInfC∧COND_718_1_MAIN_INVOKEMETHOD1(TRUE, 656_0_length_Return(x0[16]), x1[17], x2[16], java.lang.Object(List(x3[16])))≥775_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x1[17]), x2[16], x3[16], x1[17])∧(UIncreasing(775_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x1[17]), x2[17], x3[17], x1[17])), ≥))
(338) (0 ≥ 0 ⇒ (UIncreasing(775_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x1[17]), x2[17], x3[17], x1[17])), ≥)∧[(3)bni_157 + (-1)Bound*bni_157] + [(4)bni_157]x3[16] + [bni_157]x2[16] + [bni_157]x1[17] ≥ 0∧[4 + (-1)bso_158] + [3]x3[16] ≥ 0)
(339) (0 ≥ 0 ⇒ (UIncreasing(775_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x1[17]), x2[17], x3[17], x1[17])), ≥)∧[(3)bni_157 + (-1)Bound*bni_157] + [(4)bni_157]x3[16] + [bni_157]x2[16] + [bni_157]x1[17] ≥ 0∧[4 + (-1)bso_158] + [3]x3[16] ≥ 0)
(340) (0 ≥ 0 ⇒ (UIncreasing(775_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x1[17]), x2[17], x3[17], x1[17])), ≥)∧[(3)bni_157 + (-1)Bound*bni_157] + [(4)bni_157]x3[16] + [bni_157]x2[16] + [bni_157]x1[17] ≥ 0∧[4 + (-1)bso_158] + [3]x3[16] ≥ 0)
(341) (0 ≥ 0 ⇒ (UIncreasing(775_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x1[17]), x2[17], x3[17], x1[17])), ≥)∧[(4)bni_157] ≥ 0∧[bni_157] ≥ 0∧[bni_157] ≥ 0∧0 ≥ 0∧[(3)bni_157 + (-1)Bound*bni_157] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[4 + (-1)bso_158] ≥ 0∧[1] ≥ 0)
(342) (=(0, %(x0[18], 3))=TRUE∧656_0_length_Return(x0[18])=656_0_length_Return(x0[19])∧x1[18]=x1[19]∧java.lang.Object(List(x3[18]))=java.lang.Object(List(x3[19]))∧x2[18]=x2[19] ⇒ 668_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[18]), x1[18], java.lang.Object(List(x3[18])), x2[18])≥NonInfC∧668_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[18]), x1[18], java.lang.Object(List(x3[18])), x2[18])≥COND_668_1_MAIN_INVOKEMETHOD1(=(0, %(x0[18], 3)), 656_0_length_Return(x0[18]), x1[18], java.lang.Object(List(x3[18])), x2[18])∧(UIncreasing(COND_668_1_MAIN_INVOKEMETHOD1(=(0, %(x0[18], 3)), 656_0_length_Return(x0[18]), x1[18], java.lang.Object(List(x3[18])), x2[18])), ≥))
(343) (=(0, %(x0[18], 3))=TRUE ⇒ 668_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[18]), x1[18], java.lang.Object(List(x3[18])), x2[18])≥NonInfC∧668_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[18]), x1[18], java.lang.Object(List(x3[18])), x2[18])≥COND_668_1_MAIN_INVOKEMETHOD1(=(0, %(x0[18], 3)), 656_0_length_Return(x0[18]), x1[18], java.lang.Object(List(x3[18])), x2[18])∧(UIncreasing(COND_668_1_MAIN_INVOKEMETHOD1(=(0, %(x0[18], 3)), 656_0_length_Return(x0[18]), x1[18], java.lang.Object(List(x3[18])), x2[18])), ≥))
(344) (0 ≥ 0 ⇒ (UIncreasing(COND_668_1_MAIN_INVOKEMETHOD1(=(0, %(x0[18], 3)), 656_0_length_Return(x0[18]), x1[18], java.lang.Object(List(x3[18])), x2[18])), ≥)∧[(3)bni_159 + (-1)Bound*bni_159] + [bni_159]x2[18] + [(4)bni_159]x3[18] + [bni_159]x1[18] ≥ 0∧[(-1)bso_160] ≥ 0)
(345) (0 ≥ 0 ⇒ (UIncreasing(COND_668_1_MAIN_INVOKEMETHOD1(=(0, %(x0[18], 3)), 656_0_length_Return(x0[18]), x1[18], java.lang.Object(List(x3[18])), x2[18])), ≥)∧[(3)bni_159 + (-1)Bound*bni_159] + [bni_159]x2[18] + [(4)bni_159]x3[18] + [bni_159]x1[18] ≥ 0∧[(-1)bso_160] ≥ 0)
(346) (0 ≥ 0 ⇒ (UIncreasing(COND_668_1_MAIN_INVOKEMETHOD1(=(0, %(x0[18], 3)), 656_0_length_Return(x0[18]), x1[18], java.lang.Object(List(x3[18])), x2[18])), ≥)∧[(3)bni_159 + (-1)Bound*bni_159] + [bni_159]x2[18] + [(4)bni_159]x3[18] + [bni_159]x1[18] ≥ 0∧[(-1)bso_160] ≥ 0)
(347) (0 ≥ 0 ⇒ (UIncreasing(COND_668_1_MAIN_INVOKEMETHOD1(=(0, %(x0[18], 3)), 656_0_length_Return(x0[18]), x1[18], java.lang.Object(List(x3[18])), x2[18])), ≥)∧[bni_159] ≥ 0∧[(4)bni_159] ≥ 0∧[bni_159] ≥ 0∧0 ≥ 0∧[(3)bni_159 + (-1)Bound*bni_159] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_160] ≥ 0)
(348) (=(0, %(x0[18], 3))=TRUE∧656_0_length_Return(x0[18])=656_0_length_Return(x0[19])∧x1[18]=x1[19]∧java.lang.Object(List(x3[18]))=java.lang.Object(List(x3[19]))∧x2[18]=x2[19]∧233_0_length_ConstantStackPush(java.lang.Object(List(x3[19])))=656_0_length_Return(x0[4])∧x1[19]=x1[4]∧x2[19]=x2[4]∧java.lang.Object(List(x3[19]))=x3[4] ⇒ COND_668_1_MAIN_INVOKEMETHOD1(TRUE, 656_0_length_Return(x0[19]), x1[19], java.lang.Object(List(x3[19])), x2[19])≥NonInfC∧COND_668_1_MAIN_INVOKEMETHOD1(TRUE, 656_0_length_Return(x0[19]), x1[19], java.lang.Object(List(x3[19])), x2[19])≥718_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(java.lang.Object(List(x3[19]))), x1[19], x2[19], java.lang.Object(List(x3[19])))∧(UIncreasing(718_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(java.lang.Object(List(x3[19]))), x1[19], x2[19], java.lang.Object(List(x3[19])))), ≥))
(349) (=(0, %(x0[18], 3))=TRUE∧627_0_length_NULL(1, x3[19])=656_0_length_Return(x0[4]) ⇒ COND_668_1_MAIN_INVOKEMETHOD1(TRUE, 656_0_length_Return(x0[18]), x1[18], java.lang.Object(List(x3[19])), x2[18])≥NonInfC∧COND_668_1_MAIN_INVOKEMETHOD1(TRUE, 656_0_length_Return(x0[18]), x1[18], java.lang.Object(List(x3[19])), x2[18])≥718_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(java.lang.Object(List(x3[19]))), x1[18], x2[18], java.lang.Object(List(x3[19])))∧(UIncreasing(718_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(java.lang.Object(List(x3[19]))), x1[19], x2[19], java.lang.Object(List(x3[19])))), ≥))
(350) (0 ≥ 0 ⇒ (UIncreasing(718_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(java.lang.Object(List(x3[19]))), x1[19], x2[19], java.lang.Object(List(x3[19])))), ≥)∧[(3)bni_161 + (-1)Bound*bni_161] + [bni_161]x2[18] + [(4)bni_161]x3[19] + [bni_161]x1[18] ≥ 0∧[(-1)bso_162] ≥ 0)
(351) (0 ≥ 0 ⇒ (UIncreasing(718_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(java.lang.Object(List(x3[19]))), x1[19], x2[19], java.lang.Object(List(x3[19])))), ≥)∧[(3)bni_161 + (-1)Bound*bni_161] + [bni_161]x2[18] + [(4)bni_161]x3[19] + [bni_161]x1[18] ≥ 0∧[(-1)bso_162] ≥ 0)
(352) (0 ≥ 0 ⇒ (UIncreasing(718_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(java.lang.Object(List(x3[19]))), x1[19], x2[19], java.lang.Object(List(x3[19])))), ≥)∧[(3)bni_161 + (-1)Bound*bni_161] + [bni_161]x2[18] + [(4)bni_161]x3[19] + [bni_161]x1[18] ≥ 0∧[(-1)bso_162] ≥ 0)
(353) (0 ≥ 0 ⇒ (UIncreasing(718_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(java.lang.Object(List(x3[19]))), x1[19], x2[19], java.lang.Object(List(x3[19])))), ≥)∧[bni_161] ≥ 0∧[(4)bni_161] ≥ 0∧[bni_161] ≥ 0∧0 ≥ 0∧[(3)bni_161 + (-1)Bound*bni_161] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_162] ≥ 0)
(354) (=(0, %(x0[18], 3))=TRUE∧656_0_length_Return(x0[18])=656_0_length_Return(x0[19])∧x1[18]=x1[19]∧java.lang.Object(List(x3[18]))=java.lang.Object(List(x3[19]))∧x2[18]=x2[19]∧233_0_length_ConstantStackPush(java.lang.Object(List(x3[19])))=656_0_length_Return(x0[16])∧x1[19]=x1[16]∧x2[19]=x2[16]∧java.lang.Object(List(x3[19]))=java.lang.Object(List(x3[16])) ⇒ COND_668_1_MAIN_INVOKEMETHOD1(TRUE, 656_0_length_Return(x0[19]), x1[19], java.lang.Object(List(x3[19])), x2[19])≥NonInfC∧COND_668_1_MAIN_INVOKEMETHOD1(TRUE, 656_0_length_Return(x0[19]), x1[19], java.lang.Object(List(x3[19])), x2[19])≥718_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(java.lang.Object(List(x3[19]))), x1[19], x2[19], java.lang.Object(List(x3[19])))∧(UIncreasing(718_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(java.lang.Object(List(x3[19]))), x1[19], x2[19], java.lang.Object(List(x3[19])))), ≥))
(355) (=(0, %(x0[18], 3))=TRUE∧627_0_length_NULL(1, x3[19])=656_0_length_Return(x0[16]) ⇒ COND_668_1_MAIN_INVOKEMETHOD1(TRUE, 656_0_length_Return(x0[18]), x1[18], java.lang.Object(List(x3[19])), x2[18])≥NonInfC∧COND_668_1_MAIN_INVOKEMETHOD1(TRUE, 656_0_length_Return(x0[18]), x1[18], java.lang.Object(List(x3[19])), x2[18])≥718_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(java.lang.Object(List(x3[19]))), x1[18], x2[18], java.lang.Object(List(x3[19])))∧(UIncreasing(718_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(java.lang.Object(List(x3[19]))), x1[19], x2[19], java.lang.Object(List(x3[19])))), ≥))
(356) (0 ≥ 0 ⇒ (UIncreasing(718_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(java.lang.Object(List(x3[19]))), x1[19], x2[19], java.lang.Object(List(x3[19])))), ≥)∧[(3)bni_161 + (-1)Bound*bni_161] + [bni_161]x2[18] + [(4)bni_161]x3[19] + [bni_161]x1[18] ≥ 0∧[(-1)bso_162] ≥ 0)
(357) (0 ≥ 0 ⇒ (UIncreasing(718_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(java.lang.Object(List(x3[19]))), x1[19], x2[19], java.lang.Object(List(x3[19])))), ≥)∧[(3)bni_161 + (-1)Bound*bni_161] + [bni_161]x2[18] + [(4)bni_161]x3[19] + [bni_161]x1[18] ≥ 0∧[(-1)bso_162] ≥ 0)
(358) (0 ≥ 0 ⇒ (UIncreasing(718_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(java.lang.Object(List(x3[19]))), x1[19], x2[19], java.lang.Object(List(x3[19])))), ≥)∧[(3)bni_161 + (-1)Bound*bni_161] + [bni_161]x2[18] + [(4)bni_161]x3[19] + [bni_161]x1[18] ≥ 0∧[(-1)bso_162] ≥ 0)
(359) (0 ≥ 0 ⇒ (UIncreasing(718_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(java.lang.Object(List(x3[19]))), x1[19], x2[19], java.lang.Object(List(x3[19])))), ≥)∧[bni_161] ≥ 0∧[(4)bni_161] ≥ 0∧[bni_161] ≥ 0∧0 ≥ 0∧[(3)bni_161 + (-1)Bound*bni_161] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_162] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = 0
POL(233_0_length_ConstantStackPush(x1)) = 0
POL(627_0_length_NULL(x1, x2)) = 0
POL(0) = 0
POL(1100_0_test_Load(x1, x2, x3)) = x2
POL(2390_0_test_NULL(x1, x2, x3)) = 0
POL(NULL) = 0
POL(2429_0_test_Return) = 0
POL(java.lang.Object(x1)) = [2]x1
POL(List(x1)) = [2] + [2]x1
POL(3158_0_test_NULL(x1, x2, x3)) = 0
POL(656_0_length_Return(x1)) = 0
POL(Cond_627_0_length_NULL(x1, x2, x3)) = 0
POL(>=(x1, x2)) = 0
POL(+(x1, x2)) = 0
POL(1) = 0
POL(233_1_MAIN_INVOKEMETHOD(x1, x2, x3, x4)) = [-1] + x4 + x3 + x2 + [-1]x1
POL(COND_233_1_MAIN_INVOKEMETHOD(x1, x2, x3, x4, x5)) = [-1] + x5 + x4 + x3 + [-1]x2
POL(>(x1, x2)) = 0
POL(668_1_MAIN_INVOKEMETHOD(x1, x2, x3, x4)) = [-1] + x4 + x3 + x2 + [-1]x1
POL(COND_668_1_MAIN_INVOKEMETHOD(x1, x2, x3, x4, x5)) = [-1] + x5 + x4 + x3 + [-1]x2 + x1
POL(!(x1)) = 0
POL(=(x1, x2)) = 0
POL(3) = 0
POL(718_1_MAIN_INVOKEMETHOD(x1, x2, x3, x4)) = [-1] + x4 + x3 + x2 + [-1]x1
POL(COND_718_1_MAIN_INVOKEMETHOD(x1, x2, x3, x4, x5)) = [-1] + x5 + x4 + x3 + [-1]x2
POL(5) = 0
POL(775_1_MAIN_INVOKEMETHOD(x1, x2, x3, x4)) = [-1] + x4 + x3 + x2 + [-1]x1
POL(807_1_MAIN_INVOKEMETHOD(x1, x2, x3, x4, x5)) = [-1] + x5 + x3 + x2 + [-1]x1
POL(COND_807_1_MAIN_INVOKEMETHOD(x1, x2, x3, x4, x5, x6)) = [-1] + x6 + x4 + x3 + [-1]x2
POL(<=(x1, x2)) = 0
POL(867_1_MAIN_INVOKEMETHOD(x1, x2, x3, x4)) = [-1] + x4 + x3 + x2 + [-1]x1
POL(908_1_MAIN_INVOKEMETHOD(x1, x2, x3, x4, x5)) = [-1] + x5 + x3 + x2 + [-1]x1
POL(COND_908_1_MAIN_INVOKEMETHOD(x1, x2, x3, x4, x5, x6)) = [-1] + x6 + x4 + x3 + [-1]x2 + [-1]x1
POL(1100_1_MAIN_INVOKEMETHOD(x1, x2, x3, x4)) = [2] + x4 + x3 + x2
POL(COND_807_1_MAIN_INVOKEMETHOD1(x1, x2, x3, x4, x5, x6)) = [-1] + x6 + x4 + x3 + [-1]x2
POL(COND_718_1_MAIN_INVOKEMETHOD1(x1, x2, x3, x4, x5)) = [-1] + x5 + x4 + x3 + [-1]x2
POL(COND_668_1_MAIN_INVOKEMETHOD1(x1, x2, x3, x4, x5)) = [-1] + x5 + x4 + x3 + [-1]x2
COND_908_1_MAIN_INVOKEMETHOD(TRUE, 656_0_length_Return(x0[11]), x1[11], java.lang.Object(List(x3[11])), x4[11], x2[11]) → 1100_1_MAIN_INVOKEMETHOD(1100_0_test_Load(x1[11], x2[11], x3[11]), x1[11], x2[11], x3[11])
1100_1_MAIN_INVOKEMETHOD(2429_0_test_Return, x0[12], x1[12], x2[12]) → 233_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x0[12]), x1[12], x2[12], x0[12])
908_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[13]), x1[13], x3[13], x0[13], java.lang.Object(List(x2[13]))) → 1100_1_MAIN_INVOKEMETHOD(1100_0_test_Load(x1[13], x2[13], x3[13]), x1[13], x2[13], x3[13])
COND_807_1_MAIN_INVOKEMETHOD1(TRUE, 656_0_length_Return(x0[15]), java.lang.Object(List(x1[15])), x3[15], x4[15], x2[15]) → 1100_1_MAIN_INVOKEMETHOD(1100_0_test_Load(x1[15], x2[15], x3[15]), x1[15], x2[15], x3[15])
COND_718_1_MAIN_INVOKEMETHOD1(TRUE, 656_0_length_Return(x0[17]), x1[17], x2[17], java.lang.Object(List(x3[17]))) → 775_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x1[17]), x2[17], x3[17], x1[17])
233_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[0]), x2[0], x3[0], x1[0]) → COND_233_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 656_0_length_Return(x0[0]), x2[0], x3[0], x1[0])
COND_233_1_MAIN_INVOKEMETHOD(TRUE, 656_0_length_Return(x0[1]), x2[1], x3[1], x1[1]) → 668_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x3[1]), x2[1], x1[1], x3[1])
668_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[2]), x1[2], x3[2], x2[2]) → COND_668_1_MAIN_INVOKEMETHOD(!(=(%(x0[2], 3), 0)), 656_0_length_Return(x0[2]), x1[2], x3[2], x2[2])
COND_668_1_MAIN_INVOKEMETHOD(TRUE, 656_0_length_Return(x0[3]), x1[3], x3[3], x2[3]) → 718_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x3[3]), x1[3], x2[3], x3[3])
718_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[4]), x1[4], x2[4], x3[4]) → COND_718_1_MAIN_INVOKEMETHOD(!(=(%(x0[4], 5), 0)), 656_0_length_Return(x0[4]), x1[4], x2[4], x3[4])
COND_718_1_MAIN_INVOKEMETHOD(TRUE, 656_0_length_Return(x0[5]), x1[5], x2[5], x3[5]) → 775_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x1[5]), x2[5], x3[5], x1[5])
807_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[7]), x1[7], x3[7], x4[7], x2[7]) → COND_807_1_MAIN_INVOKEMETHOD(<=(x4[7], x0[7]), 656_0_length_Return(x0[7]), x1[7], x3[7], x4[7], x2[7])
COND_807_1_MAIN_INVOKEMETHOD(TRUE, 656_0_length_Return(x0[8]), x1[8], x3[8], x4[8], x2[8]) → 867_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x1[8]), x2[8], x3[8], x1[8])
908_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[10]), x1[10], java.lang.Object(List(x3[10])), x4[10], x2[10]) → COND_908_1_MAIN_INVOKEMETHOD(!(=(x4[10], x0[10])), 656_0_length_Return(x0[10]), x1[10], java.lang.Object(List(x3[10])), x4[10], x2[10])
COND_908_1_MAIN_INVOKEMETHOD(TRUE, 656_0_length_Return(x0[11]), x1[11], java.lang.Object(List(x3[11])), x4[11], x2[11]) → 1100_1_MAIN_INVOKEMETHOD(1100_0_test_Load(x1[11], x2[11], x3[11]), x1[11], x2[11], x3[11])
908_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[13]), x1[13], x3[13], x0[13], java.lang.Object(List(x2[13]))) → 1100_1_MAIN_INVOKEMETHOD(1100_0_test_Load(x1[13], x2[13], x3[13]), x1[13], x2[13], x3[13])
807_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[14]), java.lang.Object(List(x1[14])), x3[14], x4[14], x2[14]) → COND_807_1_MAIN_INVOKEMETHOD1(>(x4[14], x0[14]), 656_0_length_Return(x0[14]), java.lang.Object(List(x1[14])), x3[14], x4[14], x2[14])
COND_807_1_MAIN_INVOKEMETHOD1(TRUE, 656_0_length_Return(x0[15]), java.lang.Object(List(x1[15])), x3[15], x4[15], x2[15]) → 1100_1_MAIN_INVOKEMETHOD(1100_0_test_Load(x1[15], x2[15], x3[15]), x1[15], x2[15], x3[15])
718_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[16]), x1[16], x2[16], java.lang.Object(List(x3[16]))) → COND_718_1_MAIN_INVOKEMETHOD1(=(0, %(x0[16], 5)), 656_0_length_Return(x0[16]), x1[16], x2[16], java.lang.Object(List(x3[16])))
COND_718_1_MAIN_INVOKEMETHOD1(TRUE, 656_0_length_Return(x0[17]), x1[17], x2[17], java.lang.Object(List(x3[17]))) → 775_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x1[17]), x2[17], x3[17], x1[17])
668_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[18]), x1[18], java.lang.Object(List(x3[18])), x2[18]) → COND_668_1_MAIN_INVOKEMETHOD1(=(0, %(x0[18], 3)), 656_0_length_Return(x0[18]), x1[18], java.lang.Object(List(x3[18])), x2[18])
COND_668_1_MAIN_INVOKEMETHOD1(TRUE, 656_0_length_Return(x0[19]), x1[19], java.lang.Object(List(x3[19])), x2[19]) → 718_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(java.lang.Object(List(x3[19]))), x1[19], x2[19], java.lang.Object(List(x3[19])))
233_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[0]), x2[0], x3[0], x1[0]) → COND_233_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 656_0_length_Return(x0[0]), x2[0], x3[0], x1[0])
COND_233_1_MAIN_INVOKEMETHOD(TRUE, 656_0_length_Return(x0[1]), x2[1], x3[1], x1[1]) → 668_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x3[1]), x2[1], x1[1], x3[1])
668_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[2]), x1[2], x3[2], x2[2]) → COND_668_1_MAIN_INVOKEMETHOD(!(=(%(x0[2], 3), 0)), 656_0_length_Return(x0[2]), x1[2], x3[2], x2[2])
COND_668_1_MAIN_INVOKEMETHOD(TRUE, 656_0_length_Return(x0[3]), x1[3], x3[3], x2[3]) → 718_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x3[3]), x1[3], x2[3], x3[3])
718_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[4]), x1[4], x2[4], x3[4]) → COND_718_1_MAIN_INVOKEMETHOD(!(=(%(x0[4], 5), 0)), 656_0_length_Return(x0[4]), x1[4], x2[4], x3[4])
COND_718_1_MAIN_INVOKEMETHOD(TRUE, 656_0_length_Return(x0[5]), x1[5], x2[5], x3[5]) → 775_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x1[5]), x2[5], x3[5], x1[5])
775_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[6]), x2[6], x3[6], x1[6]) → 807_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[6]), x1[6], x3[6], x0[6], x2[6])
807_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[7]), x1[7], x3[7], x4[7], x2[7]) → COND_807_1_MAIN_INVOKEMETHOD(<=(x4[7], x0[7]), 656_0_length_Return(x0[7]), x1[7], x3[7], x4[7], x2[7])
COND_807_1_MAIN_INVOKEMETHOD(TRUE, 656_0_length_Return(x0[8]), x1[8], x3[8], x4[8], x2[8]) → 867_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x1[8]), x2[8], x3[8], x1[8])
867_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[9]), x2[9], x3[9], x1[9]) → 908_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(x2[9]), x1[9], x3[9], x0[9], x2[9])
908_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[10]), x1[10], java.lang.Object(List(x3[10])), x4[10], x2[10]) → COND_908_1_MAIN_INVOKEMETHOD(!(=(x4[10], x0[10])), 656_0_length_Return(x0[10]), x1[10], java.lang.Object(List(x3[10])), x4[10], x2[10])
807_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[14]), java.lang.Object(List(x1[14])), x3[14], x4[14], x2[14]) → COND_807_1_MAIN_INVOKEMETHOD1(>(x4[14], x0[14]), 656_0_length_Return(x0[14]), java.lang.Object(List(x1[14])), x3[14], x4[14], x2[14])
718_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[16]), x1[16], x2[16], java.lang.Object(List(x3[16]))) → COND_718_1_MAIN_INVOKEMETHOD1(=(0, %(x0[16], 5)), 656_0_length_Return(x0[16]), x1[16], x2[16], java.lang.Object(List(x3[16])))
668_1_MAIN_INVOKEMETHOD(656_0_length_Return(x0[18]), x1[18], java.lang.Object(List(x3[18])), x2[18]) → COND_668_1_MAIN_INVOKEMETHOD1(=(0, %(x0[18], 3)), 656_0_length_Return(x0[18]), x1[18], java.lang.Object(List(x3[18])), x2[18])
COND_668_1_MAIN_INVOKEMETHOD1(TRUE, 656_0_length_Return(x0[19]), x1[19], java.lang.Object(List(x3[19])), x2[19]) → 718_1_MAIN_INVOKEMETHOD(233_0_length_ConstantStackPush(java.lang.Object(List(x3[19]))), x1[19], x2[19], java.lang.Object(List(x3[19])))
233_0_length_ConstantStackPush(x0)1 ↔ 627_0_length_NULL(0, x0)1
627_0_length_NULL(x0, NULL)1 ↔ 656_0_length_Return(x0)1
627_0_length_NULL(x1, java.lang.Object(List(x0)))1 ↔ Cond_627_0_length_NULL(>=(x1, 0), x1, java.lang.Object(List(x0)))1
Cond_627_0_length_NULL(TRUE, x1, java.lang.Object(List(x0)))1 ↔ 627_0_length_NULL(+(x1, 1), x0)1
!(TRUE)1 ↔ FALSE1
!(FALSE)1 ↔ TRUE1
1100_0_test_Load(x0, x1, x2)1 → 2390_0_test_NULL(x1, x2, x0)1
2390_0_test_NULL(x0, x1, NULL)1 ↔ 2429_0_test_Return1
2390_0_test_NULL(x1, x2, java.lang.Object(List(x0)))1 ↔ 3158_0_test_NULL(java.lang.Object(List(x1)), java.lang.Object(List(x2)), x0)1
3158_0_test_NULL(java.lang.Object(List(o862)), java.lang.Object(List(o863)), o962)1 ↔ 2390_0_test_NULL(java.lang.Object(List(o862)), java.lang.Object(List(o863)), o962)1
2390_0_test_NULL(x1, x2, java.lang.Object(List(x0)))1 ↔ 2390_0_test_NULL(java.lang.Object(List(x1)), java.lang.Object(List(x2)), x0)1
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer, Boolean
(0) -> (1), if ((x0[0] > 0 →* TRUE)∧(656_0_length_Return(x0[0]) →* 656_0_length_Return(x0[1]))∧(x2[0] →* x2[1])∧(x3[0] →* x3[1])∧(x1[0] →* x1[1]))
(1) -> (2), if ((233_0_length_ConstantStackPush(x3[1]) →* 656_0_length_Return(x0[2]))∧(x2[1] →* x1[2])∧(x1[1] →* x3[2])∧(x3[1] →* x2[2]))
(2) -> (3), if ((!(x0[2] % 3 = 0) →* TRUE)∧(656_0_length_Return(x0[2]) →* 656_0_length_Return(x0[3]))∧(x1[2] →* x1[3])∧(x3[2] →* x3[3])∧(x2[2] →* x2[3]))
(3) -> (4), if ((233_0_length_ConstantStackPush(x3[3]) →* 656_0_length_Return(x0[4]))∧(x1[3] →* x1[4])∧(x2[3] →* x2[4])∧(x3[3] →* x3[4]))
(19) -> (4), if ((233_0_length_ConstantStackPush(java.lang.Object(List(x3[19]))) →* 656_0_length_Return(x0[4]))∧(x1[19] →* x1[4])∧(x2[19] →* x2[4])∧(java.lang.Object(List(x3[19])) →* x3[4]))
(4) -> (5), if ((!(x0[4] % 5 = 0) →* TRUE)∧(656_0_length_Return(x0[4]) →* 656_0_length_Return(x0[5]))∧(x1[4] →* x1[5])∧(x2[4] →* x2[5])∧(x3[4] →* x3[5]))
(5) -> (6), if ((233_0_length_ConstantStackPush(x1[5]) →* 656_0_length_Return(x0[6]))∧(x2[5] →* x2[6])∧(x3[5] →* x3[6])∧(x1[5] →* x1[6]))
(6) -> (7), if ((233_0_length_ConstantStackPush(x2[6]) →* 656_0_length_Return(x0[7]))∧(x1[6] →* x1[7])∧(x3[6] →* x3[7])∧(x0[6] →* x4[7])∧(x2[6] →* x2[7]))
(7) -> (8), if ((x4[7] <= x0[7] →* TRUE)∧(656_0_length_Return(x0[7]) →* 656_0_length_Return(x0[8]))∧(x1[7] →* x1[8])∧(x3[7] →* x3[8])∧(x4[7] →* x4[8])∧(x2[7] →* x2[8]))
(8) -> (9), if ((233_0_length_ConstantStackPush(x1[8]) →* 656_0_length_Return(x0[9]))∧(x2[8] →* x2[9])∧(x3[8] →* x3[9])∧(x1[8] →* x1[9]))
(9) -> (10), if ((233_0_length_ConstantStackPush(x2[9]) →* 656_0_length_Return(x0[10]))∧(x1[9] →* x1[10])∧(x3[9] →* java.lang.Object(List(x3[10])))∧(x0[9] →* x4[10])∧(x2[9] →* x2[10]))
(6) -> (14), if ((233_0_length_ConstantStackPush(x2[6]) →* 656_0_length_Return(x0[14]))∧(x1[6] →* java.lang.Object(List(x1[14])))∧(x3[6] →* x3[14])∧(x0[6] →* x4[14])∧(x2[6] →* x2[14]))
(3) -> (16), if ((233_0_length_ConstantStackPush(x3[3]) →* 656_0_length_Return(x0[16]))∧(x1[3] →* x1[16])∧(x2[3] →* x2[16])∧(x3[3] →* java.lang.Object(List(x3[16]))))
(19) -> (16), if ((233_0_length_ConstantStackPush(java.lang.Object(List(x3[19]))) →* 656_0_length_Return(x0[16]))∧(x1[19] →* x1[16])∧(x2[19] →* x2[16])∧(java.lang.Object(List(x3[19])) →* java.lang.Object(List(x3[16]))))
(1) -> (18), if ((233_0_length_ConstantStackPush(x3[1]) →* 656_0_length_Return(x0[18]))∧(x2[1] →* x1[18])∧(x1[1] →* java.lang.Object(List(x3[18])))∧(x3[1] →* x2[18]))
(18) -> (19), if ((0 = x0[18] % 3 →* TRUE)∧(656_0_length_Return(x0[18]) →* 656_0_length_Return(x0[19]))∧(x1[18] →* x1[19])∧(java.lang.Object(List(x3[18])) →* java.lang.Object(List(x3[19])))∧(x2[18] →* x2[19]))
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer